- syntactic: Std.Tactic.GuardExpr.MatchKind
A syntactic match means that the

`Expr`

s 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.

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

## Instances For

Default-reducibility defeq matching for `guard_hyp`

types

## Instances For

Syntactic matching for `guard_hyp`

types

## Instances For

Alpha-eq matching for `guard_hyp`

types

## Instances For

The `guard_hyp`

type specifier, one of `:`

, `:~`

, `:ₛ`

, `:ₐ`

## Instances For

Reducible defeq matching for `guard_hyp`

values

## Instances For

Default-reducibility defeq matching for `guard_hyp`

values

## Instances For

Syntactic matching for `guard_hyp`

values

## Instances For

Alpha-eq matching for `guard_hyp`

values

## Instances For

The `guard_hyp`

value specifier, one of `:=`

, `:=~`

, `:=ₛ`

, `:=ₐ`

## Instances For

Reducible defeq matching for `guard_expr`

## Instances For

Default-reducibility defeq matching for `guard_expr`

## Instances For

Syntactic matching for `guard_expr`

## Instances For

Alpha-eq matching for `guard_expr`

## Instances For

The `guard_expr`

matching specifier, one of `=`

, `=~`

, `=ₛ`

, `=ₐ`

## Instances For

Converts a `colon`

syntax into a `MatchKind`

## Instances For

Converts a `colonEq`

syntax into a `MatchKind`

## Instances For

Converts a `equal`

syntax into a `MatchKind`

## Instances For

Applies the selected matching rule to two expressions.

## Instances For

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.

## Instances For

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.

## 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).

## Instances For

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.

## 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 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.

## 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 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.

## 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 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.

## 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.

## 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.

## 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.

## Instances For

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.

## Instances For

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.

## 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`

.