Unfold definitions commonly used in well founded relation definitions.
This is primarily intended for internal use in
- tacticSimp_wf = Lean.ParserDescr.node `tacticSimp_wf 1024 (Lean.ParserDescr.nonReservedSymbol "simp_wf" false)
Extensible helper tactic for
decreasing_tactic. This handles the "base case"
reasoning after applying lexicographic order lemmas.
It can be extended by adding more macro definitions, e.g.
macro_rules | `(tactic| decreasing_trivial) => `(tactic| linarith)
- tacticDecreasing_trivial = Lean.ParserDescr.node `tacticDecreasing_trivial 1024 (Lean.ParserDescr.nonReservedSymbol "decreasing_trivial" false)
Constructs a proof of decreasing along a well founded relation, by applying
lexicographic order lemmas and using
ts to solve the base case. If it fails,
it prints a message to help the user diagnose an ill-founded recursive definition.
- One or more equations did not get rendered due to their size.
decreasing_tactic is called by default on well-founded recursions in order
to synthesize a proof that recursive calls decrease along the selected
well founded relation. It can be locally overridden by using
on the recursive definition, and it can also be globally extended by adding
more definitions for
which this tactic calls).
- tacticDecreasing_tactic = Lean.ParserDescr.node `tacticDecreasing_tactic 1024 (Lean.ParserDescr.nonReservedSymbol "decreasing_tactic" false)