Details (#30)

- FOL: add builtins for quantifier notations
- List: remove warnings
- Nat: remove non-linear rule ```$x - $x ↪ _0```

FOL.lp

@@ -6,6 +6,8 @@ require open Stdlib.Set Stdlib.Prop;
 
 constant symbol ∀ [a] : (τ a → Prop) → Prop; // !! or \forall
 
+builtin "all" ≔ ∀;
+
 notation ∀ quantifier;
 
 rule π (∀ $f) ↪ Π x, π ($f x);
@@ -14,6 +16,8 @@ rule π (∀ $f) ↪ Π x, π ($f x);
 
 constant symbol ∃ [a] : (τ a → Prop) → Prop; // ?? or \exists
 
+builtin "ex" ≔ ∃;
+
 notation ∃ quantifier;
 
 constant symbol ∃ᵢ [a p] (x:τ a) : π (p x) → π (∃ p);

List.lp

@@ -488,7 +488,7 @@ end;
 
 symbol Arr : ℕ → Set → Set → TYPE;
 
-rule Arr 0 $a $b ↪ τ $b
+rule Arr 0 _ $b ↪ τ $b
 with Arr ($n +1) $a $b ↪ τ $a → Arr $n $a $b;
 
 // seqn
@@ -505,7 +505,7 @@ assert a (x y : τ a) ⊢ seqn 2 x y ≡ x ⸬ y ⸬ □;
 // iota
 
 symbol iota : ℕ → ℕ → 𝕃 nat;
-rule iota $n 0 ↪ □
+rule iota _ 0 ↪ □
 with iota $n ($k +1) ↪ $n ⸬ iota ($n +1) $k;
 
 assert ⊢ iota 1 2 ≡ 1 ⸬ 2 ⸬ □;