Add test cases

t/code/error/confusing-identifier-overloading-comp-meta-levels.bel

@@ -0,0 +1,16 @@
+LF tm : type = ;
+
+schema ctx = tm;
+
+inductive Ex : ctype = ;
+
+%{
+  In Beluga v1, it was possible to overload identifiers appearing in the
+  meta-level and the computation-level.
+
+  This is not supported in Beluga v1.1. The numbers in comment below the
+  expression are labels indicating how variable names were being resolved in v1.
+}%
+rec f : {g : ctx} → [g ⊢ tm] → Ex → Ex =
+  mlam g ⇒ fn g ⇒ fn x ⇒ let [_ ⊢ x] = g in f [g] [g ⊢ x] x;
+%      1      2      3            4    2       1   1   4  3

t/code/error/confusing-identifier-overloading-comp-meta-levels.bel.out

@@ -0,0 +1,10 @@
+File "./t/code/error/confusing-identifier-overloading-comp-meta-levels.bel",
+line 15, column 48:
+15 |  mlam g ⇒ fn g ⇒ fn x ⇒ let [_ ⊢ x] = g in f [g] [g ⊢ x] x;
+                                                   ^            
+Error: Expected a context variable.
+       File "./t/code/error/confusing-identifier-overloading-comp-meta-levels.bel",
+       line 15, column 15:
+       15 |  mlam g ⇒ fn g ⇒ fn x ⇒ let [_ ⊢ x] = g in f [g] [g ⊢ x] x;
+                         ^                                             
+       Error: g is a bound computation variable.

t/code/error/substitution-on-non-normal-term.bel

@@ -0,0 +1,11 @@
+exp : type.
+
+eq : exp → exp → type.
+
+schema ctx = block (x : exp, t : eq x x);
+
+%{
+  The substitution `(eq M M)[..]` is not in normal form.
+  We expect `eq M[..] M[..]`.
+}%
+rec reflexivity : {g : ctx} {M : [g ⊢ exp]} [g ⊢ (eq M M)[..]] = ?;

t/code/error/substitution-on-non-normal-term.bel.out

@@ -0,0 +1,4 @@
+File "./t/code/error/substitution-on-non-normal-term.bel", line 11, column 50:
+11 |rec reflexivity : {g : ctx} {M : [g ⊢ exp]} [g ⊢ (eq M M)[..]] = ?;
+                                                     ^^^^^^^^^^^^      
+Error: Substitution terms may not appear as contextual LF types.

t/code/success/modules/user-defined-notations-in-modules.bel

@@ -0,0 +1,41 @@
+module Term = struct
+  LF term : type =
+  | lam : (term → term) → term
+  | app : term → term → term
+  | unit : term;
+
+  --name term M.
+end
+
+module Algorithmic_equality = struct
+  --open Term.
+
+  % This notation pragma is local to module `Algorithmic_equality`
+  --infix ≡ none.
+
+  LF ≡ : term → term → type =
+  | lam : ({x : term} → x ≡ x → M x ≡ N x) → Term.lam M ≡ Term.lam N
+  | app : M1 ≡ N1 → M2 ≡ N2 → Term.app M1 M2 ≡ Term.app N1 N2
+  | unit : Term.unit ≡ Term.unit;
+end
+
+--open Term.
+--open Algorithmic_equality. % This brings back the infix notation for `≡`
+
+schema ctx = block (x : term, eq : x ≡ x);
+
+rec aeq_reflexivity : (g : ctx) → {M : [g ⊢ term]} → [g ⊢ M ≡ M] =
+  / total d (aeq_reflexivity _ d) /
+  mlam M ⇒
+    case [_ ⊢ M] of
+    | [g ⊢ #p.x] ⇒ [g ⊢ #p.eq]
+    | [g ⊢ Term.lam \x. F] ⇒
+        let [g, b : block (x : term, eq : x ≡ x) ⊢ D] =
+          aeq_reflexivity [g, b : block (x : term, eq : x ≡ x) ⊢ F[.., b.x]]
+        in
+        [g ⊢ Algorithmic_equality.lam \x. \eq. D[.., <x; eq>]]
+    | [g ⊢ Term.app M1 M2] ⇒
+        let [g ⊢ D1] = aeq_reflexivity [g ⊢ M1] in
+        let [g ⊢ D2] = aeq_reflexivity [g ⊢ M2] in
+        [g ⊢ Algorithmic_equality.app D1 D2]
+    | [g ⊢ Term.unit] ⇒ [g ⊢ Algorithmic_equality.unit];