Reducible defeq matching for `guard_hyp`

types

## Equations

- Lean.Parser.colonR = Lean.ParserDescr.nodeWithAntiquot "colonR" `Lean.Parser.colonR (Lean.ParserDescr.symbol " : ")

## Instances For

Default-reducibility defeq matching for `guard_hyp`

types

## Equations

- Lean.Parser.colonD = Lean.ParserDescr.nodeWithAntiquot "colonD" `Lean.Parser.colonD (Lean.ParserDescr.symbol " :~ ")

## Instances For

Syntactic matching for `guard_hyp`

types

## Equations

- Lean.Parser.colonS = Lean.ParserDescr.nodeWithAntiquot "colonS" `Lean.Parser.colonS (Lean.ParserDescr.symbol " :ₛ ")

## Instances For

Alpha-eq matching for `guard_hyp`

types

## Equations

- Lean.Parser.colonA = Lean.ParserDescr.nodeWithAntiquot "colonA" `Lean.Parser.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

- Lean.Parser.colonEqR = Lean.ParserDescr.nodeWithAntiquot "colonEqR" `Lean.Parser.colonEqR (Lean.ParserDescr.symbol " := ")

## Instances For

Default-reducibility defeq matching for `guard_hyp`

values

## Equations

- Lean.Parser.colonEqD = Lean.ParserDescr.nodeWithAntiquot "colonEqD" `Lean.Parser.colonEqD (Lean.ParserDescr.symbol " :=~ ")

## Instances For

Syntactic matching for `guard_hyp`

values

## Equations

- Lean.Parser.colonEqS = Lean.ParserDescr.nodeWithAntiquot "colonEqS" `Lean.Parser.colonEqS (Lean.ParserDescr.symbol " :=ₛ ")

## Instances For

Alpha-eq matching for `guard_hyp`

values

## Equations

- Lean.Parser.colonEqA = Lean.ParserDescr.nodeWithAntiquot "colonEqA" `Lean.Parser.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

- Lean.Parser.equalR = Lean.ParserDescr.nodeWithAntiquot "equalR" `Lean.Parser.equalR (Lean.ParserDescr.symbol " = ")

## Instances For

Default-reducibility defeq matching for `guard_expr`

## Equations

- Lean.Parser.equalD = Lean.ParserDescr.nodeWithAntiquot "equalD" `Lean.Parser.equalD (Lean.ParserDescr.symbol " =~ ")

## Instances For

Syntactic matching for `guard_expr`

## Equations

- Lean.Parser.equalS = Lean.ParserDescr.nodeWithAntiquot "equalS" `Lean.Parser.equalS (Lean.ParserDescr.symbol " =ₛ ")

## Instances For

Alpha-eq matching for `guard_expr`

## Equations

- Lean.Parser.equalA = Lean.ParserDescr.nodeWithAntiquot "equalA" `Lean.Parser.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

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.

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

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

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

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

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

- Lean.Parser.Command.guardCmd = Lean.ParserDescr.node `Lean.Parser.Command.guardCmd 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#guard ") (Lean.ParserDescr.cat `term 0))