Ant S. (Apr 17 2026 at 14:03): Ant S. (Apr 17 2026 at 14:03):I know I can do something on the lines of define A where adef[simp]: "A ≡..." but what if I want to always rewrite A to to its right hand side, or use it in blast? (since it seems blast doesn't use this simp rule). I guess therte are two problems here: If I don't use auto/simp, how do I make the current proof context automatically rewrite the definition of A to its right-hand side? My current solution is to add using adef in any proof steps that use it, but that seems unnecessary. Is this where translation would be useful?
Mathias Fleury (Apr 17 2026 at 14:26):You can use abbreviation instead of definition
Ant S. (Apr 17 2026 at 14:27):within a proof context?
Ant S. (Apr 17 2026 at 14:27):Bad context for command "abbreviation"⌂ -- using reset state
Ant S. (Apr 17 2026 at 14:27):I get this
Maximilian Schäffeler (Apr 17 2026 at 14:40):You can use let ?x = "…"
Ant S. (Apr 17 2026 at 14:49):Thanks!
Last updated: May 05 2026 at 02:56 UTC