max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init/Grind/Ordered
History
Leonardo de Moura aab65f595d
feat: infrastructure for disequality constraints in grind linarith (#8715) 
This PR implements the basic infrastructure for processing disequalities
in the `grind linarith` module. We still have to implement backtracking.
2025-06-11 04:04:41 +00:00
..
Field.lean
Int.lean
Linarith.lean feat: infrastructure for disequality constraints in grind linarith (#8715) 2025-06-11 04:04:41 +00:00
Module.lean
Order.lean feat: CommRing interface for grind linarith (#8670) 2025-06-07 00:35:14 +00:00
Ring.lean