ink

inductive Std.Tactic.GuardExpr.MatchKind : Type

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

  syntactic: Std.Tactic.GuardExpr.MatchKind

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

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

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

  alphaEq: Std.Tactic.GuardExpr.MatchKind

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.

ink

def Std.Tactic.GuardExpr.colonR : Lean.ParserDescr

Reducible defeq matching for guard_hyp types

Equations

• Std.Tactic.GuardExpr.colonR = Lean.ParserDescr.nodeWithAntiquot "colonR" `Std.Tactic.GuardExpr.colonR (Lean.ParserDescr.symbol " : ")

ink

def Std.Tactic.GuardExpr.colonD : Lean.ParserDescr

Default-reducibility defeq matching for guard_hyp types

Equations

• Std.Tactic.GuardExpr.colonD = Lean.ParserDescr.nodeWithAntiquot "colonD" `Std.Tactic.GuardExpr.colonD (Lean.ParserDescr.symbol " :~ ")

ink

def Std.Tactic.GuardExpr.colonS : Lean.ParserDescr

Syntactic matching for guard_hyp types

Equations

• Std.Tactic.GuardExpr.colonS = Lean.ParserDescr.nodeWithAntiquot "colonS" `Std.Tactic.GuardExpr.colonS (Lean.ParserDescr.symbol " :ₛ ")

ink

def Std.Tactic.GuardExpr.colonA : Lean.ParserDescr

Alpha-eq matching for guard_hyp types

Equations

• Std.Tactic.GuardExpr.colonA = Lean.ParserDescr.nodeWithAntiquot "colonA" `Std.Tactic.GuardExpr.colonA (Lean.ParserDescr.symbol " :ₐ ")

ink

def Std.Tactic.GuardExpr.colon : Lean.ParserDescr

The guard_hyp type specifier, one of :, :~, :ₛ, :ₐ

Equations

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

ink

def Std.Tactic.GuardExpr.colonEqR : Lean.ParserDescr

Reducible defeq matching for guard_hyp values

Equations

• Std.Tactic.GuardExpr.colonEqR = Lean.ParserDescr.nodeWithAntiquot "colonEqR" `Std.Tactic.GuardExpr.colonEqR (Lean.ParserDescr.symbol " := ")

ink

def Std.Tactic.GuardExpr.colonEqD : Lean.ParserDescr

Default-reducibility defeq matching for guard_hyp values

Equations

• Std.Tactic.GuardExpr.colonEqD = Lean.ParserDescr.nodeWithAntiquot "colonEqD" `Std.Tactic.GuardExpr.colonEqD (Lean.ParserDescr.symbol " :=~ ")

ink

def Std.Tactic.GuardExpr.colonEqS : Lean.ParserDescr

Syntactic matching for guard_hyp values

Equations

• Std.Tactic.GuardExpr.colonEqS = Lean.ParserDescr.nodeWithAntiquot "colonEqS" `Std.Tactic.GuardExpr.colonEqS (Lean.ParserDescr.symbol " :=ₛ ")

ink

def Std.Tactic.GuardExpr.colonEqA : Lean.ParserDescr

Alpha-eq matching for guard_hyp values

Equations

• Std.Tactic.GuardExpr.colonEqA = Lean.ParserDescr.nodeWithAntiquot "colonEqA" `Std.Tactic.GuardExpr.colonEqA (Lean.ParserDescr.symbol " :=ₐ ")

ink

def Std.Tactic.GuardExpr.colonEq : Lean.ParserDescr

The guard_hyp value specifier, one of :=, :=~, :=ₛ, :=ₐ

Equations

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

ink

def Std.Tactic.GuardExpr.equalR : Lean.ParserDescr

Reducible defeq matching for guard_expr

Equations

• Std.Tactic.GuardExpr.equalR = Lean.ParserDescr.nodeWithAntiquot "equalR" `Std.Tactic.GuardExpr.equalR (Lean.ParserDescr.symbol " = ")

ink

def Std.Tactic.GuardExpr.equalD : Lean.ParserDescr

Default-reducibility defeq matching for guard_expr

Equations

• Std.Tactic.GuardExpr.equalD = Lean.ParserDescr.nodeWithAntiquot "equalD" `Std.Tactic.GuardExpr.equalD (Lean.ParserDescr.symbol " =~ ")

ink

def Std.Tactic.GuardExpr.equalS : Lean.ParserDescr

Syntactic matching for guard_expr

Equations

• Std.Tactic.GuardExpr.equalS = Lean.ParserDescr.nodeWithAntiquot "equalS" `Std.Tactic.GuardExpr.equalS (Lean.ParserDescr.symbol " =ₛ ")

ink

def Std.Tactic.GuardExpr.equalA : Lean.ParserDescr

Alpha-eq matching for guard_expr

Equations

• Std.Tactic.GuardExpr.equalA = Lean.ParserDescr.nodeWithAntiquot "equalA" `Std.Tactic.GuardExpr.equalA (Lean.ParserDescr.symbol " =ₐ ")

ink

def Std.Tactic.GuardExpr.equal : Lean.ParserDescr

The guard_expr matching specifier, one of =, =~, =ₛ, =ₐ

Equations

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

ink

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

Converts a colon syntax into a MatchKind

Equations

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

ink

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

Converts a colonEq syntax into a MatchKind

Equations

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

ink

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

Converts a equal syntax into a MatchKind

Equations

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

ink

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

Applies the selected matching rule to two expressions.

Equations

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

ink

def Std.Tactic.GuardExpr.guardExpr : Lean.ParserDescr

Check equality of two expressions.

• guard_expr e = e' checks that e and e' are defeq at reducible transparency.
• guard_expr e =~ e' checks that e and e' are defeq at default transparency.
• guard_expr e =ₛ e' checks that e and e' are syntactically equal.
• guard_expr e =ₐ e' checks that e and e' are alpha-equivalent.

Equations

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

ink

def Std.Tactic.GuardExpr.guardExprConv : Lean.ParserDescr

Check equality of two expressions.

• guard_expr e = e' checks that e and e' are defeq at reducible transparency.
• guard_expr e =~ e' checks that e and e' are defeq at default transparency.
• guard_expr e =ₛ e' checks that e and e' are syntactically equal.
• guard_expr e =ₐ e' checks that e and e' are alpha-equivalent.

Equations

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

ink

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

Check equality of two expressions.

• guard_expr e = e' checks that e and e' are defeq at reducible transparency.
• guard_expr e =~ e' checks that e and e' are defeq at default transparency.
• guard_expr e =ₛ e' checks that e and e' are syntactically equal.
• guard_expr e =ₐ e' checks that e and e' are alpha-equivalent.

Equations

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

ink

def Std.Tactic.GuardExpr.guardTarget : Lean.ParserDescr

Check the target agrees with a given expression.

• guard_target = e checks that the target is defeq at reducible transparency to e.
• guard_target =~ e checks that the target is defeq at default transparency to e.
• guard_target =ₛ e checks that the target is syntactically equal to e.
• guard_target =ₐ e checks that the target is alpha-equivalent to e.

Equations

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

ink

def Std.Tactic.GuardExpr.guardTargetConv : Lean.ParserDescr

Check the target agrees with a given expression.

• guard_target = e checks that the target is defeq at reducible transparency to e.
• guard_target =~ e checks that the target is defeq at default transparency to e.
• guard_target =ₛ e checks that the target is syntactically equal to e.
• guard_target =ₐ e checks that the target is alpha-equivalent to e.

Equations

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

ink

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

Check the target agrees with a given expression.

• guard_target = e checks that the target is defeq at reducible transparency to e.
• guard_target =~ e checks that the target is defeq at default transparency to e.
• guard_target =ₛ e checks that the target is syntactically equal to e.
• guard_target =ₐ e checks that the target is alpha-equivalent to e.

Equations

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

ink

def Std.Tactic.GuardExpr.guardHyp : Lean.ParserDescr

Check that a named hypothesis has a given type and/or value.

• guard_hyp h : t checks the type up to reducible defeq,
• guard_hyp h :~ t checks the type up to default defeq,
• guard_hyp h :ₛ t checks the type up to syntactic equality,
• guard_hyp h :ₐ t checks the type up to alpha equality.
• guard_hyp h := v checks value up to reducible defeq,
• guard_hyp h :=~ v checks value up to default defeq,
• guard_hyp h :=ₛ v checks value up to syntactic equality,
• guard_hyp h :=ₐ v checks the value up to alpha equality.

Equations

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

ink

def Std.Tactic.GuardExpr.guardHypConv : Lean.ParserDescr

Check that a named hypothesis has a given type and/or value.

• guard_hyp h : t checks the type up to reducible defeq,
• guard_hyp h :~ t checks the type up to default defeq,
• guard_hyp h :ₛ t checks the type up to syntactic equality,
• guard_hyp h :ₐ t checks the type up to alpha equality.
• guard_hyp h := v checks value up to reducible defeq,
• guard_hyp h :=~ v checks value up to default defeq,
• guard_hyp h :=ₛ v checks value up to syntactic equality,
• guard_hyp h :=ₐ v checks the value up to alpha equality.

Equations

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

ink

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

Check that a named hypothesis has a given type and/or value.

• guard_hyp h : t checks the type up to reducible defeq,
• guard_hyp h :~ t checks the type up to default defeq,
• guard_hyp h :ₛ t checks the type up to syntactic equality,
• guard_hyp h :ₐ t checks the type up to alpha equality.
• guard_hyp h := v checks value up to reducible defeq,
• guard_hyp h :=~ v checks value up to default defeq,
• guard_hyp h :=ₛ v checks value up to syntactic equality,
• guard_hyp h :=ₐ v checks the value up to alpha equality.

Equations

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