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

Equations

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

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

Converts a colonEq syntax into a MatchKind

Equations

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

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

Converts a equal syntax into a MatchKind

Equations

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

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

Applies the selected matching rule to two expressions.

Equations

• Lean.Elab.Tactic.GuardExpr.MatchKind.isEq a b Lean.Elab.Tactic.GuardExpr.MatchKind.syntactic = pure (a.consumeMData == b.consumeMData)
• Lean.Elab.Tactic.GuardExpr.MatchKind.isEq a b Lean.Elab.Tactic.GuardExpr.MatchKind.alphaEq = pure (a.eqv b)
• Lean.Elab.Tactic.GuardExpr.MatchKind.isEq a b (Lean.Elab.Tactic.GuardExpr.MatchKind.defEq red) = Lean.withoutModifyingState (Lean.Meta.withTransparency red (Lean.Meta.isDefEqGuarded a b))

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).

Equations

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

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

Equations

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

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

Equations

• Lean.Elab.Tactic.GuardExpr.evalGuardExprConv = Lean.Elab.Tactic.GuardExpr.evalGuardExpr

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

Equations

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

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

Equations

• Lean.Elab.Tactic.GuardExpr.evalGuardTargetConv = Lean.Elab.Tactic.GuardExpr.evalGuardTarget

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

Equations

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

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

Equations

• Lean.Elab.Tactic.GuardExpr.evalGuardHypConv = Lean.Elab.Tactic.GuardExpr.evalGuardHyp

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

Equations

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

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

Equations

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