From 37dd1ee76d868930955d734cd4edbeb82c5a2856 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 27 Mar 2023 00:08:48 +0200
Subject: [PATCH] a few tests

---
 tests/Tests/Equal.idr | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 863d4ca..6473a33 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -33,6 +33,8 @@ parameters (0 d : Nat) (ctx : TyContext Three d n)
   subTD, equalTD : Term Three d n -> Term Three d n -> Term Three d n -> M ()
   subTD ty s t = Term.sub ctx ty s t
   equalTD ty s t = Term.equal ctx ty s t
+  equalTyD : Term Three d n -> Term Three d n -> M ()
+  equalTyD s t = Term.equalType ctx s t
 
   subED, equalED : Elim Three d n -> Elim Three d n -> M ()
   subED e f = Elim.sub ctx e f
@@ -42,6 +44,8 @@ parameters (ctx : TyContext Three 0 n)
   subT, equalT : Term Three 0 n -> Term Three 0 n -> Term Three 0 n -> M ()
   subT = subTD 0 ctx
   equalT = equalTD 0 ctx
+  equalTy : Term Three 0 n -> Term Three 0 n -> M ()
+  equalTy = equalTyD 0 ctx
 
   subE, equalE : Elim Three 0 n -> Elim Three 0 n -> M ()
   subE = subED 0 ctx
@@ -418,6 +422,14 @@ tests = "equality & subtyping" :- [
         (F "f")
   ],
 
+  "natural type" :- [
+    testEq "ℕ = ℕ" $ equalTy empty Nat Nat,
+    testEq "ℕ = ℕ : ★₀" $ equalT empty (TYPE 0) Nat Nat,
+    testEq "ℕ = ℕ : ★₆₉" $ equalT empty (TYPE 69) Nat Nat,
+    testNeq "ℕ ≠ {}" $ equalTy empty Nat (enum []),
+    testEq "0=1 ⊢ ℕ = {}" $ equalTy empty01 Nat (enum [])
+  ],
+
   "natural numbers" :- [
     testEq "zero = zero" $ equalT empty Nat Zero Zero,
     testEq "succ two = succ two" $