From f988d541364841cd208f4fd21ff8e5e2935fc7aa Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 24 Jun 2021 22:40:05 +0100
Subject: Bad practice huge commit: 1. Rudimentary prototype definitional
 package 2. Started univalence 3. Various compatibility fixes and new theory
 stubs 4. Updated ROOT file

---
 mltt/core/lib.ML | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'mltt/core/lib.ML')

diff --git a/mltt/core/lib.ML b/mltt/core/lib.ML
index f15daf6..98d83cc 100644
--- a/mltt/core/lib.ML
+++ b/mltt/core/lib.ML
@@ -14,6 +14,7 @@ val dest_eq: term -> term * term
 val mk_Var: string -> int -> typ -> term
 val lambda_var: term -> term -> term
 
+val is_lvl: term -> bool
 val is_typing: term -> bool
 val mk_typing: term -> term -> term
 val dest_typing: term -> term * term
@@ -83,6 +84,8 @@ fun lambda_var x tm =
 
 (* Object *)
 
+fun is_lvl t = case fastype_of t of Type (\<^type_name>\<open>lvl\<close>, _) => true | _ => false
+
 fun is_typing (Const (\<^const_name>\<open>has_type\<close>, _) $ _ $ _) = true
   | is_typing _ = false
 
@@ -189,7 +192,6 @@ fun subterm_order t1 t2 =
   else EQUAL
 
 fun lvl_order t1 t2 =
-  let val _ = @{print} (fastype_of t1) in
   case fastype_of t1 of
     Type (\<^type_name>\<open>lvl\<close>, _) => (case fastype_of t2 of
                           Type (\<^type_name>\<open>lvl\<close>, _) => EQUAL
@@ -199,7 +201,6 @@ fun lvl_order t1 t2 =
                           Type (\<^type_name>\<open>lvl\<close>, _) => GREATER
                         | _ => EQUAL)
   | _ => EQUAL
-  end
 
 fun cond_order o1 o2 = case o1 of EQUAL => o2 | _ => o1
 
-- 
cgit v1.2.3