def SSA.tacticOnly_goal_ : Lean.ParserDescr

only_goal $t runs $t on the current goal, but only if there is a goal to be solved. Essentially, this silences "no goals to be solved" errors

Equations

• One or more equations did not get rendered due to their size.

def SSA.«tacticSimp_peephole[_,,]» : Lean.ParserDescr

simp_peephole simplifies away the framework overhead of denoting expressions/programs.

In it's bare form, it only simplifies away the core framework definitions (e.g., Expr.denote), but we can also pass it dialect-specific definitions to unfold, as in: simp_peephole [foo, bar, baz]

Equations

• One or more equations did not get rendered due to their size.

def SSA.«tacticSimp_peephole[_,,]At_» : Lean.ParserDescr

simp_peephole at ΓV simplifies away the framework overhead of denoting expressions/programs, that are evaluated with the valuation ΓV.

The actual simplification happens in the simp_peephole tactic defined above. After simplifying, the goal state should only contain occurences of valuation ΓV directly applied to some variable v : Var Γ ty. The present tactic tries to eliminate the valuation completely, by introducing a new universally quantified (Lean) variable to the goal for every (object) variable v.

Equations

• One or more equations did not get rendered due to their size.

def SSA.tacticSimp_peepholeAt_ : Lean.ParserDescr

simp_peephole with no extra user defined theorems.

Equations

• One or more equations did not get rendered due to their size.

def SSA.tacticSimp_peephole : Lean.ParserDescr

Equations

• SSA.tacticSimp_peephole = Lean.ParserDescr.node `SSA.tacticSimp_peephole 1024 (Lean.ParserDescr.nonReservedSymbol "simp_peephole" false)