0d2a574f96
This PR implements user-defined `grind` attributes. They are useful for users that want to implement tactics using the `grind` infrastructure (e.g., `progress*` in Aeneas). New `grind` attributes are declared using the command ```lean register_grind_attr my_grind ``` The command is similar to `register_simp_attr`. After the new attribute is declared. Recall that similar to `register_simp_attr`, the new attribute cannot be used in the same file it is declared. ```lean opaque f : Nat → Nat opaque g : Nat → Nat @[my_grind] theorem fax : f (f x) = f x := sorry example theorem fax2 : f (f (f x)) = f x := by fail_if_success grind grind [my_grind] ``` TODO: remove leftovers after update stage0 |
||
|---|---|---|
| .. | ||
| src | ||
| stdlib | ||