source
def Lean.Parser.colonR :
ParserDescr

Reducible defeq matching for `guard_hyp` types

Equations

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

Instances For

source
def Lean.Parser.colonD :
ParserDescr

Default-reducibility defeq matching for `guard_hyp` types

Equations

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

Instances For

source
def Lean.Parser.colonS :
ParserDescr

Syntactic matching for `guard_hyp` types

Equations

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

Instances For

source
def Lean.Parser.colonA :
ParserDescr

Alpha-eq matching for `guard_hyp` types

Equations

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

Instances For

source
def Lean.Parser.colon :
ParserDescr

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

Equations

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

Instances For

source
def Lean.Parser.colonEqR :
ParserDescr

Reducible defeq matching for `guard_hyp` values

Equations

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

Instances For

source
def Lean.Parser.colonEqD :
ParserDescr

Default-reducibility defeq matching for `guard_hyp` values

Equations

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

Instances For

source
def Lean.Parser.colonEqS :
ParserDescr

Syntactic matching for `guard_hyp` values

Equations

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

Instances For

source
def Lean.Parser.colonEqA :
ParserDescr

Alpha-eq matching for `guard_hyp` values

Equations

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

Instances For

source
def Lean.Parser.colonEq :
ParserDescr

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

Equations

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

Instances For

source
def Lean.Parser.equalR :
ParserDescr

Reducible defeq matching for `guard_expr`

Equations

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

Instances For

source
def Lean.Parser.equalD :
ParserDescr

Default-reducibility defeq matching for `guard_expr`

Equations

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

Instances For

source
def Lean.Parser.equalS :
ParserDescr

Syntactic matching for `guard_expr`

Equations

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

Instances For

source
def Lean.Parser.equalA :
ParserDescr

Alpha-eq matching for `guard_expr`

Equations

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

Instances For

source
def Lean.Parser.equal :
ParserDescr

The `guard_expr` matching specifier, one of `=`, `=~`, `=ₛ`, `=ₐ`

Equations

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

Instances For

source
def Lean.Parser.Tactic.guardExpr :
ParserDescr

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

source
def Lean.Parser.Tactic.guardExprConv :
ParserDescr

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

source
def Lean.Parser.Tactic.guardTarget :
ParserDescr

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

source
def Lean.Parser.Tactic.guardTargetConv :
ParserDescr

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

source
def Lean.Parser.Tactic.guardHyp :
ParserDescr

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

source
def Lean.Parser.Tactic.guardHypConv :
ParserDescr

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

source
def Lean.Parser.Command.guardExprCmd :
ParserDescr

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

source
def Lean.Parser.Command.guardCmd :
ParserDescr

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

Instances For