| /- | |
| Copyright (c) 2021 Microsoft Corporation. All rights reserved. | |
| Released under Apache 2.0 license as described in the file LICENSE. | |
| Authors: Gabriel Ebner | |
| -/ | |
| prelude | |
| import Init.NotationExtra | |
| namespace Lean | |
| /-- | |
| The syntax category of binder predicates contains predicates like `> 0`, `∈ s`, etc. | |
| (`: t` should not be a binder predicate because it would clash with the built-in syntax for ∀/∃.) | |
| -/ | |
| declare_syntax_cat binderPred | |
| /-- | |
| `satisfies_binder_pred% t pred` expands to a proposition expressing that `t` satisfies `pred`. | |
| -/ | |
| syntax "satisfies_binder_pred% " term:max binderPred : term | |
| -- Extend ∀ and ∃ to binder predicates. | |
| /-- | |
| The notation `∃ x < 2, p x` is shorthand for `∃ x, x < 2 ∧ p x`, | |
| and similarly for other binary operators. | |
| -/ | |
| syntax "∃ " binderIdent binderPred ", " term : term | |
| /-- | |
| The notation `∀ x < 2, p x` is shorthand for `∀ x, x < 2 → p x`, | |
| and similarly for other binary operators. | |
| -/ | |
| syntax "∀ " binderIdent binderPred ", " term : term | |
| macro_rules | |
| | `(∃ $x:ident $pred:binderPred, $p) => | |
| `(∃ $x:ident, satisfies_binder_pred% $x $pred ∧ $p) | |
| | `(∃ _ $pred:binderPred, $p) => | |
| `(∃ x, satisfies_binder_pred% x $pred ∧ $p) | |
| macro_rules | |
| | `(∀ $x:ident $pred:binderPred, $p) => | |
| `(∀ $x:ident, satisfies_binder_pred% $x $pred → $p) | |
| | `(∀ _ $pred:binderPred, $p) => | |
| `(∀ x, satisfies_binder_pred% x $pred → $p) | |
| /-- Declare `∃ x > y, ...` as syntax for `∃ x, x > y ∧ ...` -/ | |
| binder_predicate x " > " y:term => `($x > $y) | |
| /-- Declare `∃ x ≥ y, ...` as syntax for `∃ x, x ≥ y ∧ ...` -/ | |
| binder_predicate x " ≥ " y:term => `($x ≥ $y) | |
| /-- Declare `∃ x < y, ...` as syntax for `∃ x, x < y ∧ ...` -/ | |
| binder_predicate x " < " y:term => `($x < $y) | |
| /-- Declare `∃ x ≤ y, ...` as syntax for `∃ x, x ≤ y ∧ ...` -/ | |
| binder_predicate x " ≤ " y:term => `($x ≤ $y) | |
| /-- Declare `∃ x ≠ y, ...` as syntax for `∃ x, x ≠ y ∧ ...` -/ | |
| binder_predicate x " ≠ " y:term => `($x ≠ $y) | |
| /-- Declare `∀ x ∈ y, ...` as syntax for `∀ x, x ∈ y → ...` and `∃ x ∈ y, ...` as syntax for | |
| `∃ x, x ∈ y ∧ ...` -/ | |
| binder_predicate x " ∈ " y:term => `($x ∈ $y) | |
| /-- Declare `∀ x ∉ y, ...` as syntax for `∀ x, x ∉ y → ...` and `∃ x ∉ y, ...` as syntax for | |
| `∃ x, x ∉ y ∧ ...` -/ | |
| binder_predicate x " ∉ " y:term => `($x ∉ $y) | |
| /-- Declare `∀ x ⊆ y, ...` as syntax for `∀ x, x ⊆ y → ...` and `∃ x ⊆ y, ...` as syntax for | |
| `∃ x, x ⊆ y ∧ ...` -/ | |
| binder_predicate x " ⊆ " y:term => `($x ⊆ $y) | |
| /-- Declare `∀ x ⊂ y, ...` as syntax for `∀ x, x ⊂ y → ...` and `∃ x ⊂ y, ...` as syntax for | |
| `∃ x, x ⊂ y ∧ ...` -/ | |
| binder_predicate x " ⊂ " y:term => `($x ⊂ $y) | |
| /-- Declare `∀ x ⊇ y, ...` as syntax for `∀ x, x ⊇ y → ...` and `∃ x ⊇ y, ...` as syntax for | |
| `∃ x, x ⊇ y ∧ ...` -/ | |
| binder_predicate x " ⊇ " y:term => `($x ⊇ $y) | |
| /-- Declare `∀ x ⊃ y, ...` as syntax for `∀ x, x ⊃ y → ...` and `∃ x ⊃ y, ...` as syntax for | |
| `∃ x, x ⊃ y ∧ ...` -/ | |
| binder_predicate x " ⊃ " y:term => `($x ⊃ $y) | |
| end Lean |