- syntactic: Std.Tactic.GuardExpr.MatchKind
A syntactic match means that the
Expr
s are==
after strippingMData
- 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.
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
- Std.Tactic.GuardExpr.colonR = Lean.ParserDescr.nodeWithAntiquot "colonR" `Std.Tactic.GuardExpr.colonR (Lean.ParserDescr.symbol " : ")
Default-reducibility defeq matching for guard_hyp
types
Equations
- Std.Tactic.GuardExpr.colonD = Lean.ParserDescr.nodeWithAntiquot "colonD" `Std.Tactic.GuardExpr.colonD (Lean.ParserDescr.symbol " :~ ")
Syntactic matching for guard_hyp
types
Equations
- Std.Tactic.GuardExpr.colonS = Lean.ParserDescr.nodeWithAntiquot "colonS" `Std.Tactic.GuardExpr.colonS (Lean.ParserDescr.symbol " :ₛ ")
Alpha-eq matching for guard_hyp
types
Equations
- Std.Tactic.GuardExpr.colonA = Lean.ParserDescr.nodeWithAntiquot "colonA" `Std.Tactic.GuardExpr.colonA (Lean.ParserDescr.symbol " :ₐ ")
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
- Std.Tactic.GuardExpr.colonEqR = Lean.ParserDescr.nodeWithAntiquot "colonEqR" `Std.Tactic.GuardExpr.colonEqR (Lean.ParserDescr.symbol " := ")
Default-reducibility defeq matching for guard_hyp
values
Equations
- Std.Tactic.GuardExpr.colonEqD = Lean.ParserDescr.nodeWithAntiquot "colonEqD" `Std.Tactic.GuardExpr.colonEqD (Lean.ParserDescr.symbol " :=~ ")
Syntactic matching for guard_hyp
values
Equations
- Std.Tactic.GuardExpr.colonEqS = Lean.ParserDescr.nodeWithAntiquot "colonEqS" `Std.Tactic.GuardExpr.colonEqS (Lean.ParserDescr.symbol " :=ₛ ")
Alpha-eq matching for guard_hyp
values
Equations
- Std.Tactic.GuardExpr.colonEqA = Lean.ParserDescr.nodeWithAntiquot "colonEqA" `Std.Tactic.GuardExpr.colonEqA (Lean.ParserDescr.symbol " :=ₐ ")
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
- Std.Tactic.GuardExpr.equalR = Lean.ParserDescr.nodeWithAntiquot "equalR" `Std.Tactic.GuardExpr.equalR (Lean.ParserDescr.symbol " = ")
Default-reducibility defeq matching for guard_expr
Equations
- Std.Tactic.GuardExpr.equalD = Lean.ParserDescr.nodeWithAntiquot "equalD" `Std.Tactic.GuardExpr.equalD (Lean.ParserDescr.symbol " =~ ")
Syntactic matching for guard_expr
Equations
- Std.Tactic.GuardExpr.equalS = Lean.ParserDescr.nodeWithAntiquot "equalS" `Std.Tactic.GuardExpr.equalS (Lean.ParserDescr.symbol " =ₛ ")
Alpha-eq matching for guard_expr
Equations
- Std.Tactic.GuardExpr.equalA = Lean.ParserDescr.nodeWithAntiquot "equalA" `Std.Tactic.GuardExpr.equalA (Lean.ParserDescr.symbol " =ₐ ")
The guard_expr
matching specifier, one of =
, =~
, =ₛ
, =ₐ
Equations
- One or more equations did not get rendered due to their size.
Converts a colon
syntax into a MatchKind
Equations
- One or more equations did not get rendered due to their size.
Converts a colonEq
syntax into a MatchKind
Equations
- One or more equations did not get rendered due to their size.
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 thate
ande'
are defeq at reducible transparency.guard_expr e =~ e'
checks thate
ande'
are defeq at default transparency.guard_expr e =ₛ e'
checks thate
ande'
are syntactically equal.guard_expr e =ₐ e'
checks thate
ande'
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 thate
ande'
are defeq at reducible transparency.guard_expr e =~ e'
checks thate
ande'
are defeq at default transparency.guard_expr e =ₛ e'
checks thate
ande'
are syntactically equal.guard_expr e =ₐ e'
checks thate
ande'
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 thate
ande'
are defeq at reducible transparency.guard_expr e =~ e'
checks thate
ande'
are defeq at default transparency.guard_expr e =ₛ e'
checks thate
ande'
are syntactically equal.guard_expr e =ₐ e'
checks thate
ande'
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 toe
.guard_target =~ e
checks that the target is defeq at default transparency toe
.guard_target =ₛ e
checks that the target is syntactically equal toe
.guard_target =ₐ e
checks that the target is alpha-equivalent toe
.
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 toe
.guard_target =~ e
checks that the target is defeq at default transparency toe
.guard_target =ₛ e
checks that the target is syntactically equal toe
.guard_target =ₐ e
checks that the target is alpha-equivalent toe
.
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 toe
.guard_target =~ e
checks that the target is defeq at default transparency toe
.guard_target =ₛ e
checks that the target is syntactically equal toe
.guard_target =ₐ e
checks that the target is alpha-equivalent toe
.
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.