# Documentation

Std.Tactic.GuardExpr

• 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:
• 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.

Instances For

Reducible defeq matching for guard_hyp types

Equations

Default-reducibility defeq matching for guard_hyp types

Equations

Syntactic matching for guard_hyp types

Equations

Alpha-eq matching for guard_hyp types

Equations

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

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

Reducible defeq matching for guard_hyp values

Equations

Default-reducibility defeq matching for guard_hyp values

Equations

Syntactic matching for guard_hyp values

Equations

Alpha-eq matching for guard_hyp values

Equations

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

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

Reducible defeq matching for guard_expr

Equations

Default-reducibility defeq matching for guard_expr

Equations

Syntactic matching for guard_expr

Equations

Alpha-eq matching for guard_expr

Equations

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

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

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

Converts a equal syntax into a MatchKind

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

Applies the selected matching rule to two expressions.

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

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.

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.

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.

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.

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.

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.

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.

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.

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.