Reservoir

joehendrix/lean-arith-solver

None Description

GitHub Link Documentation

Pick a version!

TODO: should show a time axes that allows the users to view, filter and click copy the lakefile config.

README

This repository contains some experimental code aimed at solving arithmetic problems in Lean 4.

It currently consists of a normalization routine that maps arithmetic predicates and terms into a normal form so that the solver has fewer special cases to addresss.