From 0caf3ff5144ee1697a1ae6c34f63c1acc239a6b4 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Wed, 21 Aug 2024 16:10:15 +0200
Subject: [PATCH] coq: remove type_unit & type_num

---
 coq/equiv.v | 17 ++---------------
 coq/terms.v |  2 --
 2 files changed, 2 insertions(+), 17 deletions(-)

diff --git a/coq/equiv.v b/coq/equiv.v
index 680fad3..39c8e96 100644
--- a/coq/equiv.v
+++ b/coq/equiv.v
@@ -224,9 +224,7 @@ Qed.
 
 (** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
 Inductive type_is_flat : type_term -> Prop :=
-  | FlatUnit : (type_is_flat type_unit)
   | FlatVar : forall x, (type_is_flat (type_var x))
-  | FlatNum : forall x, (type_is_flat (type_num x))
   | FlatId : forall x, (type_is_flat (type_id x))
   | FlatApp : forall x y,
     (type_is_flat x) ->
@@ -295,22 +293,11 @@ Proof.
   intros.
   destruct t.
 
-  exists type_unit.
-  split. apply TEq_Refl.
-  apply LNF.
-  admit.
-  
   exists (type_id s).
   split. apply TEq_Refl.
   apply LNF.
   admit.
   admit.
-  
-  exists (type_num n).
-  split. apply TEq_Refl.
-  apply LNF.
-  admit.
-  
   admit.
   
   exists (type_univ s t).
@@ -342,11 +329,11 @@ Admitted.
  *)
 
 Example example_flat_type :
-    (type_is_flat (type_spec (type_id "PosInt") (type_num 10))).
+    (type_is_flat (type_spec (type_id "PosInt") (type_id "10"))).
 Proof.
     apply FlatApp.
     apply FlatId.
-    apply FlatNum.
+    apply FlatId.
 Qed.
 
 Example example_lnf_type :
diff --git a/coq/terms.v b/coq/terms.v
index b998fa7..21ff0d1 100644
--- a/coq/terms.v
+++ b/coq/terms.v
@@ -8,10 +8,8 @@ Module Terms.
 
 (* types *)
 Inductive type_term : Type :=
-  | type_unit : type_term
   | type_id : string -> type_term
   | type_var : string -> type_term
-  | type_num : nat -> type_term
   | type_fun : type_term -> type_term -> type_term
   | type_univ : string -> type_term -> type_term
   | type_spec : type_term -> type_term -> type_term