- 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 " : ")
Instances For
Default-reducibility defeq matching for guard_hyp
types
Equations
- Std.Tactic.GuardExpr.colonD = Lean.ParserDescr.nodeWithAntiquot "colonD" `Std.Tactic.GuardExpr.colonD (Lean.ParserDescr.symbol " :~ ")
Instances For
Syntactic matching for guard_hyp
types
Equations
- Std.Tactic.GuardExpr.colonS = Lean.ParserDescr.nodeWithAntiquot "colonS" `Std.Tactic.GuardExpr.colonS (Lean.ParserDescr.symbol " :ₛ ")
Instances For
Alpha-eq matching for guard_hyp
types
Equations
- Std.Tactic.GuardExpr.colonA = Lean.ParserDescr.nodeWithAntiquot "colonA" `Std.Tactic.GuardExpr.colonA (Lean.ParserDescr.symbol " :ₐ ")
Instances For
The guard_hyp
type specifier, one of :
, :~
, :ₛ
, :ₐ
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reducible defeq matching for guard_hyp
values
Equations
- Std.Tactic.GuardExpr.colonEqR = Lean.ParserDescr.nodeWithAntiquot "colonEqR" `Std.Tactic.GuardExpr.colonEqR (Lean.ParserDescr.symbol " := ")
Instances For
Default-reducibility defeq matching for guard_hyp
values
Equations
- Std.Tactic.GuardExpr.colonEqD = Lean.ParserDescr.nodeWithAntiquot "colonEqD" `Std.Tactic.GuardExpr.colonEqD (Lean.ParserDescr.symbol " :=~ ")
Instances For
Syntactic matching for guard_hyp
values
Equations
- Std.Tactic.GuardExpr.colonEqS = Lean.ParserDescr.nodeWithAntiquot "colonEqS" `Std.Tactic.GuardExpr.colonEqS (Lean.ParserDescr.symbol " :=ₛ ")
Instances For
Alpha-eq matching for guard_hyp
values
Equations
- Std.Tactic.GuardExpr.colonEqA = Lean.ParserDescr.nodeWithAntiquot "colonEqA" `Std.Tactic.GuardExpr.colonEqA (Lean.ParserDescr.symbol " :=ₐ ")
Instances For
The guard_hyp
value specifier, one of :=
, :=~
, :=ₛ
, :=ₐ
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reducible defeq matching for guard_expr
Equations
- Std.Tactic.GuardExpr.equalR = Lean.ParserDescr.nodeWithAntiquot "equalR" `Std.Tactic.GuardExpr.equalR (Lean.ParserDescr.symbol " = ")
Instances For
Default-reducibility defeq matching for guard_expr
Equations
- Std.Tactic.GuardExpr.equalD = Lean.ParserDescr.nodeWithAntiquot "equalD" `Std.Tactic.GuardExpr.equalD (Lean.ParserDescr.symbol " =~ ")
Instances For
Syntactic matching for guard_expr
Equations
- Std.Tactic.GuardExpr.equalS = Lean.ParserDescr.nodeWithAntiquot "equalS" `Std.Tactic.GuardExpr.equalS (Lean.ParserDescr.symbol " =ₛ ")
Instances For
Alpha-eq matching for guard_expr
Equations
- Std.Tactic.GuardExpr.equalA = Lean.ParserDescr.nodeWithAntiquot "equalA" `Std.Tactic.GuardExpr.equalA (Lean.ParserDescr.symbol " =ₐ ")
Instances For
The guard_expr
matching specifier, one of =
, =~
, =ₛ
, =ₐ
Equations
- One or more equations did not get rendered due to their size.
Instances For
Converts a colon
syntax into a MatchKind
Equations
- One or more equations did not get rendered due to their size.
Instances For
Converts a colonEq
syntax into a MatchKind
Equations
- One or more equations did not get rendered due to their size.
Instances For
Converts a equal
syntax into a MatchKind
Equations
- One or more equations did not get rendered due to their size.
Instances For
Applies the selected matching rule to two expressions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Tactic to 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.
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.
Instances For
Tactic to 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.
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.
Instances For
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.
Instances For
Tactic to 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.
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.
Instances For
Tactic to check that 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
.
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.
Instances For
Tactic to check that 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
.
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.
Instances For
Tactic to check that 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
.
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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
Command to 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.
This is a command version of the guard_expr
tactic.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Command to 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.
This is a command version of the guard_expr
tactic.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.