inductive Std.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: Std.Tactic.GuardExpr.MatchKind

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

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

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

• alphaEq: Std.Tactic.GuardExpr.MatchKind

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

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 " : ")

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 " :~ ")

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 " :ₛ ")

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 " :ₐ ")

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.

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 " := ")

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 " :=~ ")

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 " :=ₛ ")

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 " :=ₐ ")

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.

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 " = ")

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 " =~ ")

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 " =ₛ ")

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 " =ₐ ")

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.

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.

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.

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.

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.

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

Tactic to 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.

Both e and e' are elaborated then have their metavariables instantiated before the equality check. Their types are unified (using isDefEqGuarded) before synthetic metavariables are processed, which helps with default instance handling.

Equations

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

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

Tactic to 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.

Both e and e' are elaborated then have their metavariables instantiated before the equality check. Their types are unified (using isDefEqGuarded) before synthetic metavariables are processed, which helps with default instance handling.

Equations

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

def Std.Tactic.GuardExpr.elabAndEvalMatchKind (mk : Std.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 Std.Tactic.GuardExpr.evalGuardExpr : Lean.Elab.Tactic.Tactic

Tactic to 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.

Both e and e' are elaborated then have their metavariables instantiated before the equality check. Their types are unified (using isDefEqGuarded) before synthetic metavariables are processed, which helps with default instance handling.

Equations

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

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

Tactic to check that 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.

The term e is elaborated with the type of the goal as the expected type, which is mostly useful within conv mode.

Equations

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

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

Tactic to check that 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.

The term e is elaborated with the type of the goal as the expected type, which is mostly useful within conv mode.

Equations

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

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

Tactic to check that 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.

The term e is elaborated with the type of the goal as the expected type, which is mostly useful within conv mode.

Equations

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

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

Tactic to 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.

The value v is elaborated using the type of h as the expected type.

Equations

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

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

Tactic to 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.

The value v is elaborated using the type of h as the expected type.

Equations

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

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

Tactic to 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.

The value v is elaborated using the type of h as the expected type.

Equations

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

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

Command to 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.

This is a command version of the guard_expr tactic.

Equations

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

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

Command to 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.

This is a command version of the guard_expr tactic.

Equations

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

def Std.Tactic.GuardExpr.«command#guard_» : Lean.ParserDescr

Command to check that an expression evaluates to true.

#guard e elaborates e ensuring its type is Bool then evaluates e and checks that the result is true. The term is elaborated without variables declared using variable, since these cannot be evaluated.

Since this makes use of coercions, so long as a proposition p is decidable, one can write #guard p rather than #guard decide p. A consequence to this is that if there is decidable equality one can write #guard a = b. Note that this is not exactly the same as checking if a and b evaluate to the same thing since it uses the DecidableEq instance to do the evaluation.

Note: this uses the untrusted evaluator, so #guard passing is not a proof that the expression equals true.

Equations

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