inductive Lean.Elab.Tactic.GuardExpr.MatchKind : Type

The various guard_* tactics have similar matching specifiers for how equal expressions have to be to pass the tactic. This inductive gives the different specifiers that can be selected.

• syntactic : MatchKind

  A syntactic match means that the Exprs are == after stripping MData

• defEq (red : Meta.TransparencyMode := Meta.TransparencyMode.reducible) : MatchKind

  A defeq match isDefEqGuarded returns true. (Note that unification is allowed here.)

• alphaEq : MatchKind

  An alpha-eq match means that Expr.eqv returns true.

def Lean.Elab.Tactic.GuardExpr.colon.toMatchKind : TSyntax `Lean.Parser.colon → Option MatchKind

Converts a colon syntax into a MatchKind

def Lean.Elab.Tactic.GuardExpr.colonEq.toMatchKind : TSyntax `Lean.Parser.colonEq → Option MatchKind

Converts a colonEq syntax into a MatchKind

def Lean.Elab.Tactic.GuardExpr.equal.toMatchKind : TSyntax `Lean.Parser.equal → Option MatchKind

Converts a equal syntax into a MatchKind

def Lean.Elab.Tactic.GuardExpr.MatchKind.isEq (a b : Expr) : MatchKind → MetaM Bool

Applies the selected matching rule to two expressions.

def Lean.Elab.Tactic.GuardExpr.elabAndEvalMatchKind (mk : MatchKind) (a b : Term) : TermElabM Bool

Elaborate a and b and then do the given equality test mk. We make sure to unify the types of a and b after elaboration so that when synthesizing pending metavariables we don't get the wrong instances due to default instances (for example, for nat literals).

def Lean.Elab.Tactic.GuardExpr.evalGuardExpr : Tactic

def Lean.Elab.Tactic.GuardExpr.evalGuardExprConv : Tactic

def Lean.Elab.Tactic.GuardExpr.evalGuardTarget : Tactic

def Lean.Elab.Tactic.GuardExpr.evalGuardTargetConv : Tactic

def Lean.Elab.Tactic.GuardExpr.evalGuardHyp : Tactic

def Lean.Elab.Tactic.GuardExpr.evalGuardHypConv : Tactic

def Lean.Elab.Tactic.GuardExpr.evalGuardExprCmd : Command.CommandElab

def Lean.Elab.Tactic.GuardExpr.evalGuardCmd : Command.CommandElab