diff options
author | Josh Chen | 2021-06-24 22:40:05 +0100 |
---|---|---|
committer | Josh Chen | 2021-06-24 22:40:05 +0100 |
commit | f988d541364841cd208f4fd21ff8e5e2935fc7aa (patch) | |
tree | 8ccc4d4e4cdde7572453ac0e250a224fe8db3da1 /mltt/core/lib.ML | |
parent | 0085798a86a35e2430a97289e894724f688db435 (diff) |
Bad practice huge commit:
1. Rudimentary prototype definitional package
2. Started univalence
3. Various compatibility fixes and new theory stubs
4. Updated ROOT file
Diffstat (limited to '')
-rw-r--r-- | mltt/core/lib.ML | 5 |
1 files changed, 3 insertions, 2 deletions
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 |