lean4-htt/stage0
Leonardo de Moura 71991296e0
feat: add not_value constraint to grind_pattern (#11520)
This PR implements the constraint `not_value x` in the `grind_pattern`
command. It is the negation of the constraint `is_value`.
2025-12-05 04:19:34 +00:00
..
src feat: add not_value constraint to grind_pattern (#11520) 2025-12-05 04:19:34 +00:00
stdlib chore: update stage0 2025-12-04 15:52:42 +00:00