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: Lean.Elab.Tactic.GuardExpr.MatchKind

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

• defEq: optParam Lean.Meta.TransparencyMode Lean.Meta.TransparencyMode.reducible → Lean.Elab.Tactic.GuardExpr.MatchKind

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

• alphaEq: Lean.Elab.Tactic.GuardExpr.MatchKind

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

def Lean.Elab.Tactic.GuardExpr.colon.toMatchKind : Lean.TSyntax `Lean.Parser.colon → Option Lean.Elab.Tactic.GuardExpr.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 : Lean.TSyntax `Lean.Parser.colonEq → Option Lean.Elab.Tactic.GuardExpr.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 : Lean.TSyntax `Lean.Parser.equal → Option Lean.Elab.Tactic.GuardExpr.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 : Lean.Expr) (b : Lean.Expr) : Lean.Elab.Tactic.GuardExpr.MatchKind → Lean.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 : Lean.Elab.Tactic.GuardExpr.MatchKind) (a : Lean.Term) (b : Lean.Term) : Lean.Elab.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 : Lean.Elab.Tactic.Tactic

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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