Documentation

Lean.Meta.Tactic.FVarSubst

Some tactics substitute hypotheses with expressions. We track these substitutions using FVarSubst. It is just a mapping from the original FVarId (internal) name to an expression. The free variables occurring in the expression must be defined in the new goal.

Instances For
Equations
  • s.isEmpty = s.map.isEmpty

Add entry fvarId |-> v to s if s does not contain an entry for fvarId.

Equations
  • s.insert fvarId v = if s.contains fvarId = true then s else let map := Lean.AssocList.mapVal (fun (e : Lean.Expr) => e.replaceFVarId fvarId v) s.map; { map := map.insert fvarId v }
Equations

Given e, for each (x => v) in s replace x with v in e

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

Constructs a substitution consisting of s followed by t. This satisfies (s.append t).apply e = t.apply (s.apply e)

@[reducible, inline]
Equations