[Git][monnier/typer][location-sinfo] 2 commits: save results AG - Typer

10 Jan 2023


      Ismaila FALL pushed to branch location-sinfo at Stefan / Typer
Commits:
c6d01ef4 by Fallismaila at 2023-01-10T05:26:12+00:00
save results AG
- - - - -
842b294a by Fallismaila at 2023-01-10T05:30:33+00:00
save results AG
- - - - -
15 changed files:
- + result_10.txt
- + result_100.txt
- + result_20.txt
- + result_200.txt
- + result_50.txt
- + result_500.txt
- src/REPL.ml
- src/debruijn.ml
- src/elab.ml
- src/heuristic.ml
- src/inverse_subst.ml
- src/lexp.ml
- src/opslexp.ml
- src/pexp.ml
- typer.sh
Changes:
=====================================
result_10.txt
=====================================
The diff for this file was not included because it is too large.
=====================================
result_100.txt
=====================================
The diff for this file was not included because it is too large.
=====================================
result_20.txt
=====================================
The diff for this file was not included because it is too large.
=====================================
result_200.txt
=====================================
The diff for this file was not included because it is too large.
=====================================
result_50.txt
=====================================
The diff for this file was not included because it is too large.
=====================================
result_500.txt
=====================================
@@ -0,0 +1,1415 @@
+    ================================ TYPER REPL ================================
+      Typer 0.0.0 - Interpreter - (c) 2016-2021
+
+      %quit         (%q) : leave REPL
+      %help         (%h) : print help
+    ----------------------------------------------------------------------------
+  In[00] >>     ============================== LEXP CONTEXT : ==============================
+    =============================== Proba = 1/2 ===============================
+    =============================== Popu = 500 ===============================
+    | NAME       | LEXP_UNPARSE |  TYPE                                      | 
+    ----------------------------------------------------------------------------
+ |   Option       | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) -> (##Type_ ℓ[32m[1][0m)
+
+(##_≡>_ (_:_ ℓ TypeLevel) (##_->_ (_:_ a (##Type_ ℓ)) (##Type_ ℓ)))
+
+ |   some         | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (a[32m[0][0m -> (Option[32m[103][0m ℓ[32m[2][0m a[32m[1][0m))
+
+(##_≡>_ (_:_ ℓ TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ a (Option a))))
+
+ |   none         | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (Option[32m[102][0m ℓ[32m[1][0m a[32m[0][0m)
+
+(##_≡>_ (_:_ ℓ TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (Option a)))
+
+ |   optionally   | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[1][0m)) ≡> (b : (##Type_ ℓ[32m[1][0m)) ≡> ((a[32m[1][0m -> b[32m[1][0m) -> (b[32m[1][0m -> ((Option[32m[106][0m ℓ[32m[5][0m a[32m[3][0m) -> b[32m[3][0m)))
+ crossover --> (##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_≡>_ (_:_ b (##Type_ ℓ)) (##_->_ (##_->_ a b) (##_->_ b (##_->_ (Option a) b)))))))
+
+ |   List_leng…   | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> ((List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m) -> Int[32m[255][0m)
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (List a) Int)))
+
+ |   List_head1   | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (xs : (List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m)) -> (Option[32m[103][0m ℓ[32m[2][0m a[32m[1][0m)
+
+(##_≡>_ (_:_ ℓ TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (_:_ xs (List a)) (Option a))))
+
+ |   List_head    | 
+(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ[32m[0][0m)) ≡> (x : τ[32m[0][0m) -> (xs : (List[32m[158][0m ℓ[32m[2][0m τ[32m[1][0m)) -> τ[32m[2][0m
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ τ (##Type_ ℓ)) (##_->_ (_:_ x τ) (##_->_ (_:_ xs (List τ)) τ))))
+
+ |   List_tail    | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (xs : (List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m)) -> (List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m)
+
+(##_≡>_ (_:_ ℓ TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (_:_ xs (List a)) (List a))))
+
+ |   List_map     | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[1][0m)) ≡> (b : (##Type_ ℓ[32m[1][0m)) ≡> ((a[32m[1][0m -> b[32m[1][0m) -> ((List[32m[160][0m ℓ[32m[4][0m a[32m[2][0m) -> (List[32m[161][0m ℓ[32m[4][0m b[32m[2][0m)))
+ crossover --> (##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_≡>_ (_:_ b (##Type_ ℓ)) (##_->_ (##_->_ a b) (##_->_ (List a) (List b)))))))
+
+ |   List_foldr   | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (b : (##Type_ ℓ[32m[1][0m)) ≡> (a : (##Type_ ℓ[32m[1][0m)) ≡> ((b[32m[1][0m -> (a[32m[1][0m -> a[32m[2][0m)) -> ((List[32m[160][0m ℓ[32m[4][0m b[32m[2][0m) -> (a[32m[2][0m -> a[32m[3][0m)))
+ crossover --> (##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ b (##Type_ ℓ)) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (##_->_ b (##_->_ a a)) (##_->_ (List b) (##_->_ a a)))))))
+
+ |   List_find    | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> ((a[32m[0][0m -> Bool[32m[211][0m) -> ((List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m) -> (Option[32m[104][0m ℓ[32m[3][0m a[32m[2][0m)))
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (##_->_ a Bool) (##_->_ (List a) (Option a)))))
+
+ |   List_nth     | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (Int[32m[254][0m -> ((List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m) -> (a[32m[2][0m -> a[32m[3][0m)))
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ Int (##_->_ (List a) (##_->_ a a)))))
+
+ |   Sexp_error   | 
+Sexp[32m[249][0m
+
+Sexp
+
+ |   Sexp_to_l…   | 
+(s : ##Sexp) -> (exceptions : (List[32m[156][0m ##TypeLevel.z ##Sexp)) -> (List[32m[157][0m ##TypeLevel.z ##Sexp)
+
+(##_->_ (_:_ s ##Sexp) (##_->_ (_:_ exceptions (List ##Sexp)) (List ##Sexp)))
+
+ |   multiarg_…   | 
+(name : ##String) -> (margs : (List[32m[156][0m ##TypeLevel.z Sexp[32m[250][0m)) -> (IO[32m[255][0m ##Sexp)
+
+(##_->_ (_:_ name ##String) (##_->_ (_:_ margs (List Sexp)) (IO ##Sexp)))
+
+ |   lambda_->_   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   lambda_=>_   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   lambda_…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   List_reve…   | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> ((List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m) -> ((List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m) -> (List[32m[159][0m ℓ[32m[3][0m a[32m[2][0m)))
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (List a) (##_->_ (List a) (List a)))))
+
+ |   List_conc…   | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (l : (List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m)) -> (t : (List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m)) -> (List[32m[159][0m ℓ[32m[3][0m a[32m[2][0m)
+
+(##_≡>_ (_:_ ℓ TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (_:_ l (List a)) (##_->_ (_:_ t (List a)) (List a)))))
+
+ |   List_foldl   | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[1][0m)) ≡> (b : (##Type_ ℓ[32m[1][0m)) ≡> ((a[32m[1][0m -> (b[32m[1][0m -> a[32m[3][0m)) -> (a[32m[2][0m -> ((List[32m[161][0m ℓ[32m[4][0m b[32m[2][0m) -> a[32m[4][0m)))
+ crossover --> (##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_≡>_ (_:_ b (##Type_ ℓ)) (##_->_ (##_->_ a (##_->_ b a)) (##_->_ a (##_->_ (List b) a)))))))
+
+ |   List_mapi    | 
+(a : Type[32m[245][0m) ≡> (b : Type[32m[246][0m) ≡> ((a[32m[1][0m -> (Int[32m[255][0m -> b[32m[2][0m)) -> ((List[32m[158][0m ##TypeLevel.z a[32m[2][0m) -> (List[32m[159][0m ##TypeLevel.z b[32m[2][0m)))
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (##_->_ a (##_->_ Int b)) (##_->_ (List a) (List b)))))
+
+ |   List_map2    | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[2][0m)) ≡> (b : (##Type_ ℓ[32m[2][0m)) ≡> (c : (##Type_ ℓ[32m[2][0m)) ≡> ((a[32m[2][0m -> (b[32m[2][0m -> c[32m[2][0m)) -> ((List[32m[162][0m ℓ[32m[6][0m a[32m[3][0m) -> ((List[32m[163][0m ℓ[32m[6][0m b[32m[3][0m) -> (List[32m[164][0m ℓ[32m[6][0m c[32m[3][0m))))
+ crossover --> (##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_≡>_ (_:_ b (##Type_ ℓ)) (##_≡>_ (_:_ c (##Type_ ℓ)) (##_->_ (##_->_ a (##_->_ b c)) (##_->_ (List a) (##_->_ (List b) (List c))))))))))
+
+ |   List_fold2   | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[2][0m)) ≡> (b : (##Type_ ℓ[32m[2][0m)) ≡> (c : (##Type_ ℓ[32m[2][0m)) ≡> ((a[32m[2][0m -> (b[32m[2][0m -> (c[32m[2][0m -> a[32m[5][0m))) -> (a[32m[3][0m -> ((List[32m[163][0m ℓ[32m[6][0m b[32m[3][0m) -> ((List[32m[164][0m ℓ[32m[6][0m c[32m[3][0m) -> a[32m[6][0m))))
+ crossover --> (##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_≡>_ (_:_ b (##Type_ ℓ)) (##_≡>_ (_:_ c (##Type_ ℓ)) (##_->_ (##_->_ a (##_->_ b (##_->_ c a))) (##_->_ a (##_->_ (List b) (##_->_ (List c) a))))))))))
+
+ |   List_empty   | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> ((List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m) -> Bool[32m[211][0m)
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (List a) Bool)))
+
+ |   I            | 
+(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ[32m[0][0m)) ≡> (x : τ[32m[0][0m) -> τ[32m[1][0m
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ τ (##Type_ ℓ)) (##_->_ (_:_ x τ) τ)))
+
+ |   K            | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (a[32m[0][0m -> (b : Type[32m[248][0m) ≡> (b[32m[0][0m -> a[32m[3][0m))
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ a (##_≡>_ (_:_ b Type) (##_->_ b a)))))
+
+ |   quote1       | 
+(Sexp[32m[249][0m -> Sexp[32m[250][0m)
+
+(##_->_ Sexp Sexp)
+
+ |   quote        | 
+Macro[32m[146][0m
+
+Macro
+
+ |   make-decl    | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> Sexp[32m[251][0m))
+
+(##_->_ Sexp (##_->_ Sexp Sexp))
+
+ |   chain-decl   | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> Sexp[32m[251][0m))
+
+(##_->_ Sexp (##_->_ Sexp Sexp))
+
+ |   chain-dec…   | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> (Sexp[32m[251][0m -> Sexp[32m[252][0m)))
+
+(##_->_ Sexp (##_->_ Sexp (##_->_ Sexp Sexp)))
+
+ |   make-cons    | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> Sexp[32m[251][0m))
+
+(##_->_ Sexp (##_->_ Sexp Sexp))
+
+ |   make-ann     | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> Sexp[32m[251][0m))
+
+(##_->_ Sexp (##_->_ Sexp Sexp))
+
+ |   type-impl    | 
+(x : (List[32m[155][0m ##TypeLevel.z Sexp[32m[249][0m)) -> (IO[32m[254][0m ##Sexp)
+
+(##_->_ (_:_ x (List Sexp)) (IO ##Sexp))
+
+ |   type_        | 
+Macro[32m[146][0m
+
+Macro
+
+ |   Sexp_wrap…   | 
+Type[32m[245][0m
+
+Type
+
+ |   node         | 
+(Sexp[32m[249][0m -> ((List[32m[156][0m ##TypeLevel.z Sexp[32m[250][0m) -> Sexp_wrapper[32m[66][0m))
+
+(##_->_ Sexp (##_->_ (List Sexp) Sexp_wrapper))
+
+ |   symbol       | 
+(String[32m[246][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ String Sexp_wrapper)
+
+ |   string       | 
+(String[32m[246][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ String Sexp_wrapper)
+
+ |   integer      | 
+(Integer[32m[251][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ Integer Sexp_wrapper)
+
+ |   float        | 
+(Float[32m[254][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ Float Sexp_wrapper)
+
+ |   block        | 
+(Sexp[32m[249][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ Sexp Sexp_wrapper)
+
+ |   Sexp_wrap    | 
+(s : ##Sexp) -> [35mtypecons[0m (Sexp_wrapper)   (block Sexp[32m[250][0m) (float Float[32m[255][0m) (integer Integer[32m[252][0m) (node Sexp[32m[250][0m (List[32m[157][0m ##TypeLevel.z Sexp[32m[251][0m)) (string String[32m[247][0m) (symbol String[32m[247][0m)
+
+(##_->_ (_:_ s ##Sexp) (##typecons (Sexp_wrapper) (block Sexp) (float Float) (integer Integer) (node Sexp (List Sexp)) (string String) (symbol String)))
+
+ |   BoolMod      | 
+([35mlambda [0m(t1 : (##Type_ (##TypeLevel.succ ##TypeLevel.z))) -> [35mlambda [0m(t2 : (##Type_ ##TypeLevel.z)) -> [35mlambda [0m(t3 : (##Type_ ##TypeLevel.z)) -> [35mtypecons[0m (_)   (cons t1[32m[2][0m t2[32m[2][0m t3[32m[2][0m) (##Type_ ##TypeLevel.z) [35mtypecons[0m (Bool)   (false) (true) [35mtypecons[0m (Bool)   (false) (true))
+
+((##lambda_->_ (_:_ t1 (##Type_ (##TypeLevel.succ ##TypeLevel_z))) (##lambda_->_ (_:_ t2 (##Type_ ##TypeLevel_z)) (##lambda_->_ (_:_ t3 (##Type_ ##TypeLevel_z)) (##typecons (_) (cons (_::_ t t1) (_::_ true t2) (_::_ false t3)))))) (##Type_ ##TypeLevel_z) (typecons Bool true false) (typecons Bool true false))
+
+ |   Pair         | 
+(a : Type[32m[245][0m) -> (b : Type[32m[246][0m) -> (##Type_ ##TypeLevel.z)
+
+(##_->_ (_:_ a Type) (##_->_ (_:_ b Type) (##Type_ ##TypeLevel_z)))
+
+ |   pair         | 
+(a : Type[32m[245][0m) ≡> (b : Type[32m[246][0m) ≡> (fst : a[32m[1][0m) -> (snd : b[32m[1][0m) -> (Pair[32m[59][0m a[32m[3][0m b[32m[2][0m)
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (_:_ fst a) (##_->_ (_:_ snd b) (Pair a b)))))
+
+ |   Triplet      | 
+(a : Type[32m[245][0m) -> (b : Type[32m[246][0m) -> (c : Type[32m[247][0m) -> Type[32m[248][0m
+
+(##_->_ (_:_ a Type) (##_->_ (_:_ b Type) (##_->_ (_:_ c Type) Type)))
+
+ |   triplet      | 
+(a : Type[32m[245][0m) ≡> (b : Type[32m[246][0m) ≡> (c : Type[32m[247][0m) ≡> (x : a[32m[2][0m) -> (y : b[32m[2][0m) -> (z : c[32m[2][0m) -> (Triplet[32m[59][0m a[32m[5][0m b[32m[4][0m c[32m[3][0m)
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_≡>_ (_:_ c Type) (##_->_ (_:_ x a) (##_->_ (_:_ y b) (##_->_ (_:_ z c) (Triplet a b c)))))))
+
+ |   List_merge   | 
+(a : (##Type_ ##TypeLevel.z)) ≡> (b : (##Type_ ##TypeLevel.z)) ≡> ((List[32m[157][0m ##TypeLevel.z a[32m[1][0m) -> ((List[32m[158][0m ##TypeLevel.z b[32m[1][0m) -> (List[32m[159][0m ##TypeLevel.z (Pair[32m[59][0m a[32m[3][0m b[32m[2][0m))))
+
+(##_≡>_ (_:_ a (##Type_ ##TypeLevel_z)) (##_≡>_ (_:_ b (##Type_ ##TypeLevel_z)) (##_->_ (List a) (##_->_ (List b) (List (Pair a b))))))
+
+ |   List_map-…   | 
+(τ : (##Type_ ##TypeLevel.z)) ≡> (b : Type[32m[246][0m) ≡> (xs : (List[32m[157][0m ##TypeLevel.z (Pair[32m[57][0m τ[32m[1][0m b[32m[0][0m))) -> (List[32m[158][0m ##TypeLevel.z τ[32m[2][0m)
+
+(##_≡>_ (_:_ τ (##Type_ ##TypeLevel_z)) (##_≡>_ (_:_ b Type) (##_->_ (_:_ xs (List (Pair τ b))) (List τ))))
+
+ |   List_map-…   | 
+(a : Type[32m[245][0m) ≡> (τ : (##Type_ ##TypeLevel.z)) ≡> (xs : (List[32m[157][0m ##TypeLevel.z (Pair[32m[57][0m a[32m[1][0m τ[32m[0][0m))) -> (List[32m[158][0m ##TypeLevel.z τ[32m[1][0m)
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ τ (##Type_ ##TypeLevel_z)) (##_->_ (_:_ xs (List (Pair a τ))) (List τ))))
+
+ |   False        | 
+(##Type_ ##TypeLevel.z)
+
+(##Type_ ##TypeLevel_z)
+
+ |   True         | 
+(##Type_ ##TypeLevel.z)
+
+(##Type_ ##TypeLevel_z)
+
+ |   Not          | 
+(ℓ : ##TypeLevel) ≡> (prop : (##Type_ ℓ[32m[0][0m)) -> (##Type_ ℓ[32m[1][0m)
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_->_ (_:_ prop (##Type_ ℓ)) (##Type_ ℓ)))
+
+ |   Decidable    | 
+(ℓ : ##TypeLevel) => (prop : (##Type_ ℓ[32m[0][0m)) -> (##Type_ ℓ[32m[1][0m)
+
+(##_=>_ (_:_ ℓ ##TypeLevel) (##_->_ (_:_ prop (##Type_ ℓ)) (##Type_ ℓ)))
+
+ |   LList        | 
+(Type[32m[245][0m -> (Int[32m[253][0m -> Type[32m[247][0m))
+
+(##_->_ Type (##_->_ Int Type))
+
+ |   vnil         | 
+(a : Type[32m[245][0m) ≡> (n : Int[32m[253][0m) ≡> (p : (Eq[32m[259][0m ##TypeLevel.z ##Int n[32m[0][0m (Integer->Int[32m[185][0m [33m0[0m))) ≡> (LList[32m[47][0m a[32m[2][0m n[32m[1][0m)
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ n Int) (##_≡>_ (_:_ p (Eq n (Integer->Int 0))) (LList a n))))
+
+ |   vcons        | 
+(a : Type[32m[245][0m) ≡> (n : Int[32m[253][0m) ≡> (n1 : Int[32m[254][0m) ≡> (a[32m[2][0m -> ((LList[32m[48][0m a[32m[3][0m n1[32m[1][0m) -> (p : (Eq[32m[262][0m ##TypeLevel.z ##Int n[32m[3][0m (Int_+[32m[210][0m n1[32m[2][0m (Integer->Int[32m[188][0m [33m1[0m)))) ≡> (LList[32m[50][0m a[32m[5][0m n[32m[4][0m)))
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ n Int) (##_≡>_ (_:_ n1 Int) (##_->_ a (##_->_ (LList a n1) (##_≡>_ (_:_ p (Eq n (Int_+ n1 (Integer->Int 1)))) (LList a n)))))))
+
+ |   if_then_e…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   not          | 
+(Bool[32m[208][0m -> Bool[32m[209][0m)
+
+(##_->_ Bool Bool)
+
+ |   or           | 
+(Bool[32m[208][0m -> (Bool[32m[209][0m -> Bool[32m[210][0m))
+
+(##_->_ Bool (##_->_ Bool Bool))
+
+ |   and          | 
+(Bool[32m[208][0m -> (Bool[32m[209][0m -> Bool[32m[210][0m))
+
+(##_->_ Bool (##_->_ Bool Bool))
+
+ |   xor          | 
+(Bool[32m[208][0m -> (Bool[32m[209][0m -> Bool[32m[210][0m))
+
+(##_->_ Bool (##_->_ Bool Bool))
+
+ |   fold         | 
+(Bool[32m[208][0m -> (a : Type[32m[246][0m) ≡> (a[32m[0][0m -> (a[32m[1][0m -> a[32m[2][0m)))
+
+(##_->_ Bool (##_≡>_ (_:_ a Type) (##_->_ a (##_->_ a a))))
+
+ |   test1        | 
+(Option[32m[100][0m ##TypeLevel.z Int[32m[252][0m)
+
+(Option Int)
+
+ |   test2        | 
+(Option[32m[100][0m ##TypeLevel.z Int[32m[252][0m)
+
+(Option Int)
+
+ |   test3        | 
+(Option[32m[100][0m ##TypeLevel.z Int[32m[252][0m)
+
+(Option Int)
+
+ |   test4        | 
+(Option[32m[100][0m ##TypeLevel.z Int[32m[252][0m)
+
+(Option Int)
+
+ |   Elab_nth-…   | 
+(a : ##String) -> (b : ##Int) -> (c : ##Elab_Context) -> (Option[32m[103][0m ##TypeLevel.z ##String)
+
+(##_->_ (_:_ a ##String) (##_->_ (_:_ b ##Int) (##_->_ (_:_ c ##Elab_Context) (Option ##String))))
+
+ |   Elab_arg-…   | 
+(a : ##String) -> (b : ##String) -> (c : ##Elab_Context) -> (Option[32m[103][0m ##TypeLevel.z ##Int)
+
+(##_->_ (_:_ a ##String) (##_->_ (_:_ b ##String) (##_->_ (_:_ c ##Elab_Context) (Option ##Int))))
+
+ |   poly-lits    | 
+[35mtypecons[0m (record)   (cons (α : Type[32m[245][0m) -> Type[32m[246][0m (α : Type[32m[246][0m) ≡> (fromInteger : (Integer[32m[253][0m -> α[32m[1][0m)) -> ([35mlet [0mFromInteger : (α : Type[32m[248][0m) -> Type[32m[249][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[249][0m))  (mkFromInteger (Integer[32m[256][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[249][0m))  (mkFromInteger (Integer[32m[256][0m -> α[32m[1][0m)) α[32m[1][0m) (α : Type[32m[247][0m) ≡> (inst : ([35mlet [0mFromInteger : (α : Type[32m[248][0m) -> Type[32m[249][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[249][0m))  (mkFromInteger (Integer[32m[256][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[249][0m))  (mkFromInteger (Integer[32m[256][0m -> α[32m[1][0m)) α[32m[0][0m)) => (Integer[32m[255][0m -> α[32m[2][0m) Macro[32m[149][0m ([35mlet [0mFromInteger : (α : Type[32m[249][0m) -> Type[32m[250][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[250][0m))  (mkFromInteger (Integer[32m[257][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[250][0m))  (mkFromInteger (Integer[32m[257][0m -> α[32m[1][0m)) Integer[32m[255][0m) ([35mlet [0mFromInteger : (α : Type[32m[250][0m) -> Type[32m[251][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[251][0m))  (mkFromInteger (Integer[32m[258][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[251][0m))  (mkFromInteger (Integer[32m[258][0m -> α[32m[1][0m)) Int[32m[257][0m))
+
+(##typecons (record) (cons (_::_ FromInteger (##_->_ (_:_ α Type) Type)) (_::_ mkFromInteger (##_≡>_ (_:_ α Type) (##_->_ (_:_ fromInteger (##_->_ Integer α)) ((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) α)))) (_::_ fromInteger (##_≡>_ (_:_ α Type) (##_=>_ (_:_ inst ((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) α)) (##_->_ Integer α)))) (_::_ typer-immediate Macro) (_::_ IntegerFromInteger ((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) Integer)) (_::_ IntFromInteger ((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) Int))))
+
+ |   typer-imm…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   FromInteg…   | 
+(α : Type[32m[245][0m) -> Type[32m[246][0m
+
+(##_->_ (_:_ α Type) Type)
+
+ |   mkFromInt…   | 
+(α : Type[32m[245][0m) ≡> (fromInteger : (Integer[32m[252][0m -> α[32m[1][0m)) -> ([35mlet [0mFromInteger : (α : Type[32m[247][0m) -> Type[32m[248][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[248][0m))  (mkFromInteger (Integer[32m[255][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[248][0m))  (mkFromInteger (Integer[32m[255][0m -> α[32m[1][0m)) α[32m[1][0m)
+
+(##_≡>_ (_:_ α Type) (##_->_ (_:_ fromInteger (##_->_ Integer α)) ((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) α)))
+
+ |   fromInteg…   | 
+(α : Type[32m[245][0m) ≡> (inst : ([35mlet [0mFromInteger : (α : Type[32m[246][0m) -> Type[32m[247][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[247][0m))  (mkFromInteger (Integer[32m[254][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[247][0m))  (mkFromInteger (Integer[32m[254][0m -> α[32m[1][0m)) α[32m[0][0m)) => (Integer[32m[253][0m -> α[32m[2][0m)
+
+(##_≡>_ (_:_ α Type) (##_=>_ (_:_ inst ((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) α)) (##_->_ Integer α)))
+
+ |   IntFromIn…   | 
+([35mlet [0mFromInteger : (α : Type[32m[245][0m) -> Type[32m[246][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[246][0m))  (mkFromInteger (Integer[32m[253][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[246][0m))  (mkFromInteger (Integer[32m[253][0m -> α[32m[1][0m)) Int[32m[252][0m)
+
+((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) Int)
+
+ |   IntegerFr…   | 
+([35mlet [0mFromInteger : (α : Type[32m[245][0m) -> Type[32m[246][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[246][0m))  (mkFromInteger (Integer[32m[253][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[246][0m))  (mkFromInteger (Integer[32m[253][0m -> α[32m[1][0m)) Integer[32m[251][0m)
+
+((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) Integer)
+
+ |   monads       | 
+[35mtypecons[0m (record)   (cons (M : (Type[32m[245][0m -> Type[32m[246][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)) (M : (Type[32m[246][0m -> Type[32m[247][0m)) ≡> (bind : (a : Type[32m[247][0m) ≡> (b : Type[32m[248][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m)))) -> (pure : (a : Type[32m[248][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) -> ([35mlet [0mMonad : (M : (Type[32m[249][0m -> Type[32m[250][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) M[32m[2][0m) (M : (Type[32m[247][0m -> Type[32m[248][0m)) ≡> (monad : ([35mlet [0mMonad : (M : (Type[32m[248][0m -> Type[32m[249][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[249][0m -> Type[32m[250][0m)))  (mkMonad (a : Type[32m[250][0m) ≡> (b : Type[32m[251][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[251][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[249][0m -> Type[32m[250][0m)))  (mkMonad (a : Type[32m[250][0m) ≡> (b : Type[32m[251][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[251][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) M[32m[0][0m)) => (a : Type[32m[249][0m) ≡> (b : Type[32m[250][0m) ≡> ((M[32m[3][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[5][0m b[32m[2][0m)) -> (M[32m[5][0m b[32m[2][0m))) (M : (Type[32m[248][0m -> Type[32m[249][0m)) ≡> (monad : ([35mlet [0mMonad : (M : (Type[32m[249][0m -> Type[32m[250][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) M[32m[0][0m)) => (a : Type[32m[250][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)) ([35mlet [0mMonad : (M : (Type[32m[249][0m -> Type[32m[250][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) IO[32m[257][0m) (a : Type[32m[250][0m) ≡> (b : Type[32m[251][0m) ≡> ((Option[32m[107][0m ##TypeLevel.z a[32m[1][0m) -> ((a[32m[2][0m -> (Option[32m[109][0m ##TypeLevel.z b[32m[2][0m)) -> (Option[32m[109][0m ##TypeLevel.z b[32m[2][0m))) (a : Type[32m[251][0m) ≡> (a[32m[0][0m -> (Option[32m[108][0m ##TypeLevel.z a[32m[1][0m)) ([35mlet [0mMonad : (M : (Type[32m[252][0m -> Type[32m[253][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[253][0m -> Type[32m[254][0m)))  (mkMonad (a : Type[32m[254][0m) ≡> (b : Type[32m[255][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[255][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[253][0m -> Type[32m[254][0m)))  (mkMonad (a : Type[32m[254][0m) ≡> (b : Type[32m[255][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[255][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) (Option[32m[107][0m ##TypeLevel.z)))
+ crossover --> (##typecons (record) (cons (_::_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_::_ mkMonad (##_≡>_ (_:_ M (##_->_ Type Type)) (##_->_ (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (##_->_ (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))) ((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) M))))) (_::_ bind (##_≡>_ (_:_ M (##_->_ Type Type)) (##_=>_ (_:_ monad ((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) M)) (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))))) (_::_ pure (##_≡>_ (_:_ M (##_->_ Type Type)) (##_=>_ (_:_ monad ((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) M)) (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))) (_::_ IO_monad ((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) IO)) (_::_ Option_bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (Option a) (##_->_ (##_->_ a (Option b)) (Option b)))))) (_::_ Option_pure (##_≡>_ (_:_ a Type) (##_->_ a (Option a)))) (_::_ Option_monad ((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) (Option)))))
+
+ |   Monad        | 
+(M : (Type[32m[245][0m -> Type[32m[246][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z))
+ crossover --> (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))
+
+ |   bind         | 
+(M : (Type[32m[245][0m -> Type[32m[246][0m)) ≡> (monad : ([35mlet [0mMonad : (M : (Type[32m[246][0m -> Type[32m[247][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[247][0m -> Type[32m[248][0m)))  (mkMonad (a : Type[32m[248][0m) ≡> (b : Type[32m[249][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[249][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[247][0m -> Type[32m[248][0m)))  (mkMonad (a : Type[32m[248][0m) ≡> (b : Type[32m[249][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[249][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) M[32m[0][0m)) => (a : Type[32m[247][0m) ≡> (b : Type[32m[248][0m) ≡> ((M[32m[3][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[5][0m b[32m[2][0m)) -> (M[32m[5][0m b[32m[2][0m)))
+
+(##_≡>_ (_:_ M (##_->_ Type Type)) (##_=>_ (_:_ monad ((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) M)) (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))))
+
+ |   pure         | 
+(M : (Type[32m[245][0m -> Type[32m[246][0m)) ≡> (monad : ([35mlet [0mMonad : (M : (Type[32m[246][0m -> Type[32m[247][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[247][0m -> Type[32m[248][0m)))  (mkMonad (a : Type[32m[248][0m) ≡> (b : Type[32m[249][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[249][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[247][0m -> Type[32m[248][0m)))  (mkMonad (a : Type[32m[248][0m) ≡> (b : Type[32m[249][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[249][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) M[32m[0][0m)) => (a : Type[32m[247][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))
+
+(##_≡>_ (_:_ M (##_->_ Type Type)) (##_=>_ (_:_ monad ((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) M)) (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))
+
+ |   IO_monad     | 
+([35mlet [0mMonad : (M : (Type[32m[245][0m -> Type[32m[246][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[246][0m -> Type[32m[247][0m)))  (mkMonad (a : Type[32m[247][0m) ≡> (b : Type[32m[248][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[248][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[246][0m -> Type[32m[247][0m)))  (mkMonad (a : Type[32m[247][0m) ≡> (b : Type[32m[248][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[248][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) IO[32m[253][0m)
+
+((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) IO)
+
+ |   Option_mo…   | 
+([35mlet [0mMonad : (M : (Type[32m[245][0m -> Type[32m[246][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[246][0m -> Type[32m[247][0m)))  (mkMonad (a : Type[32m[247][0m) ≡> (b : Type[32m[248][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[248][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[246][0m -> Type[32m[247][0m)))  (mkMonad (a : Type[32m[247][0m) ≡> (b : Type[32m[248][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[248][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) (Option[32m[100][0m ##TypeLevel.z))
+
+((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) (Option))
+
+ |   list         | 
+[35mtypecons[0m (record)   (cons (a : Type[32m[245][0m) ≡> ((List[32m[156][0m ##TypeLevel.z a[32m[0][0m) -> Int[32m[254][0m) (a : Type[32m[246][0m) ≡> ((List[32m[157][0m ##TypeLevel.z a[32m[0][0m) -> (Option[32m[103][0m ##TypeLevel.z a[32m[1][0m)) (a : Type[32m[247][0m) ≡> ((List[32m[158][0m ##TypeLevel.z a[32m[0][0m) -> (Option[32m[104][0m ##TypeLevel.z a[32m[1][0m)) (a : Type[32m[248][0m) ≡> ((List[32m[159][0m ##TypeLevel.z a[32m[0][0m) -> (List[32m[160][0m ##TypeLevel.z a[32m[1][0m)) (a : Type[32m[249][0m) ≡> (b : Type[32m[250][0m) ≡> ((a[32m[1][0m -> b[32m[1][0m) -> ((List[32m[162][0m ##TypeLevel.z a[32m[2][0m) -> (List[32m[163][0m ##TypeLevel.z b[32m[2][0m))) (a : Type[32m[250][0m) ≡> (b : Type[32m[251][0m) ≡> ((a[32m[1][0m -> (Int[32m[260][0m -> b[32m[2][0m)) -> ((List[32m[163][0m ##TypeLevel.z a[32m[2][0m) -> (List[32m[164][0m ##TypeLevel.z b[32m[2][0m))) (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> (c : Type[32m[253][0m) ≡> ((a[32m[2][0m -> (b[32m[2][0m -> c[32m[2][0m)) -> ((List[32m[165][0m ##TypeLevel.z a[32m[3][0m) -> ((List[32m[166][0m ##TypeLevel.z b[32m[3][0m) -> (List[32m[167][0m ##TypeLevel.z c[32m[3][0m)))) (a : Type[32m[252][0m) ≡> (b : Type[32m[253][0m) ≡> ((a[32m[1][0m -> (b[32m[1][0m -> (Int[32m[263][0m -> a[32m[4][0m))) -> (a[32m[2][0m -> ((List[32m[166][0m ##TypeLevel.z b[32m[2][0m) -> a[32m[4][0m))) (a : Type[32m[253][0m) ≡> (b : Type[32m[254][0m) ≡> (c : Type[32m[255][0m) ≡> ((a[32m[2][0m -> (b[32m[2][0m -> (c[32m[2][0m -> a[32m[5][0m))) -> (a[32m[3][0m -> ((List[32m[168][0m ##TypeLevel.z b[32m[3][0m) -> ((List[32m[169][0m ##TypeLevel.z c[32m[3][0m) -> a[32m[6][0m)))) (a : Type[32m[254][0m) ≡> (b : Type[32m[255][0m) ≡> ((b[32m[0][0m -> (a[32m[2][0m -> a[32m[3][0m)) -> ((List[32m[167][0m ##TypeLevel.z b[32m[1][0m) -> (a[32m[3][0m -> a[32m[4][0m))) (a : Type[32m[255][0m) ≡> ((a[32m[0][0m -> Bool[32m[220][0m) -> ((List[32m[167][0m ##TypeLevel.z a[32m[1][0m) -> (Option[32m[113][0m ##TypeLevel.z a[32m[2][0m))) (a : Type[32m[256][0m) ≡> (Int[32m[264][0m -> ((List[32m[168][0m ##TypeLevel.z a[32m[1][0m) -> (a[32m[2][0m -> a[32m[3][0m))) (a : Type[32m[257][0m) ≡> ((List[32m[168][0m ##TypeLevel.z a[32m[0][0m) -> ((List[32m[169][0m ##TypeLevel.z a[32m[1][0m) -> (List[32m[170][0m ##TypeLevel.z a[32m[2][0m))) (a : Type[32m[258][0m) ≡> ((List[32m[169][0m ##TypeLevel.z a[32m[0][0m) -> ((List[32m[170][0m ##TypeLevel.z a[32m[1][0m) -> (List[32m[171][0m ##TypeLevel.z a[32m[2][0m))) (a : Type[32m[259][0m) ≡> (b : Type[32m[260][0m) ≡> ((a[32m[1][0m -> (b[32m[1][0m -> a[32m[3][0m)) -> (a[32m[2][0m -> ((List[32m[173][0m ##TypeLevel.z b[32m[2][0m) -> a[32m[4][0m))) (a : Type[32m[260][0m) ≡> ((a[32m[0][0m -> Bool[32m[225][0m) -> ((List[32m[172][0m ##TypeLevel.z a[32m[1][0m) -> (List[32m[173][0m ##TypeLevel.z a[32m[2][0m))) (a : Type[32m[261][0m) ≡> (b : Type[32m[262][0m) ≡> ((List[32m[173][0m ##TypeLevel.z a[32m[1][0m) -> ((List[32m[174][0m ##TypeLevel.z b[32m[1][0m) -> (List[32m[175][0m ##TypeLevel.z (Pair[32m[75][0m a[32m[3][0m b[32m[2][0m)))) (a : Type[32m[262][0m) ≡> (b : Type[32m[263][0m) ≡> ((List[32m[174][0m ##TypeLevel.z (Pair[32m[74][0m a[32m[1][0m b[32m[0][0m)) -> (List[32m[175][0m ##TypeLevel.z a[32m[2][0m)) (a : Type[32m[263][0m) ≡> (b : Type[32m[264][0m) ≡> ((List[32m[175][0m ##TypeLevel.z (Pair[32m[75][0m a[32m[1][0m b[32m[0][0m)) -> (List[32m[176][0m ##TypeLevel.z b[32m[1][0m)) (a : Type[32m[264][0m) ≡> ((List[32m[175][0m ##TypeLevel.z a[32m[0][0m) -> Bool[32m[229][0m) (a : Type[32m[265][0m) ≡> ((a[32m[0][0m -> (a[32m[1][0m -> Bool[32m[231][0m)) -> ((List[32m[177][0m ##TypeLevel.z a[32m[1][0m) -> (List[32m[178][0m ##TypeLevel.z a[32m[2][0m))) (a : Type[32m[266][0m) ≡> ((a[32m[0][0m -> (a[32m[1][0m -> Bool[32m[232][0m)) -> ((a[32m[1][0m -> Bool[32m[232][0m) -> (a[32m[2][0m -> ((List[32m[180][0m ##TypeLevel.z a[32m[3][0m) -> (Option[32m[126][0m ##TypeLevel.z a[32m[4][0m))))) (a : Type[32m[267][0m) ≡> ((a[32m[0][0m -> Bool[32m[232][0m) -> ((List[32m[179][0m ##TypeLevel.z a[32m[1][0m) -> (List[32m[180][0m ##TypeLevel.z a[32m[2][0m))) (a : Type[32m[268][0m) ≡> ((a[32m[0][0m -> (a[32m[1][0m -> Bool[32m[234][0m)) -> ((a[32m[1][0m -> Bool[32m[234][0m) -> (a[32m[2][0m -> ((List[32m[182][0m ##TypeLevel.z a[32m[3][0m) -> Bool[32m[236][0m)))) (a : Type[32m[269][0m) ≡> ((a[32m[0][0m -> (a[32m[1][0m -> Bool[32m[235][0m)) -> (a[32m[1][0m -> ((List[32m[182][0m ##TypeLevel.z a[32m[2][0m) -> (List[32m[183][0m ##TypeLevel.z a[32m[3][0m)))) (a : Type[32m[270][0m) ≡> ((a[32m[0][0m -> (a[32m[1][0m -> Bool[32m[236][0m)) -> (a[32m[1][0m -> ((List[32m[183][0m ##TypeLevel.z a[32m[2][0m) -> (List[32m[184][0m ##TypeLevel.z a[32m[3][0m)))) (a : Type[32m[271][0m) ≡> ((a[32m[0][0m -> (a[32m[1][0m -> Bool[32m[237][0m)) -> (a[32m[1][0m -> ((List[32m[184][0m ##TypeLevel.z a[32m[2][0m) -> (List[32m[185][0m ##TypeLevel.z a[32m[3][0m)))) (a : Type[32m[272][0m) ≡> ((List[32m[183][0m ##TypeLevel.z a[32m[0][0m) -> (Array[32m[290][0m a[32m[1][0m)))
+
+(##typecons (record) (cons (_::_ length (##_≡>_ (_:_ a Type) (##_->_ (List a) Int))) (_::_ head1 (##_≡>_ (_:_ a Type) (##_->_ (List a) (Option a)))) (_::_ head (##_≡>_ (_:_ a Type) (##_->_ (List a) (Option a)))) (_::_ tail (##_≡>_ (_:_ a Type) (##_->_ (List a) (List a)))) (_::_ map (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (##_->_ a b) (##_->_ (List a) (List b)))))) (_::_ mapi (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (##_->_ a (##_->_ Int b)) (##_->_ (List a) (List b)))))) (_::_ map2 (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_≡>_ (_:_ c Type) (##_->_ (##_->_ a (##_->_ b c)) (##_->_ (List a) (##_->_ (List b) (List c)))))))) (_::_ foldli (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (##_->_ a (##_->_ b (##_->_ Int a))) (##_->_ a (##_->_ (List b) a)))))) (_::_ fold2 (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_≡>_ (_:_ c Type) (##_->_ (##_->_ a (##_->_ b (##_->_ c a))) (##_->_ a (##_->_ (List b) (##_->_ (List c) a)))))))) (_::_ foldr (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (##_->_ b (##_->_ a a)) (##_->_ (List b) (##_->_ a a)))))) (_::_ find (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a Bool) (##_->_ (List a) (Option a))))) (_::_ nth (##_≡>_ (_:_ a Type) (##_->_ Int (##_->_ (List a) (##_->_ a a))))) (_::_ reverse (##_≡>_ (_:_ a Type) (##_->_ (List a) (##_->_ (List a) (List a))))) (_::_ concat (##_≡>_ (_:_ a Type) (##_->_ (List a) (##_->_ (List a) (List a))))) (_::_ foldl (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (##_->_ a (##_->_ b a)) (##_->_ a (##_->_ (List b) a)))))) (_::_ remove (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a Bool) (##_->_ (List a) (List a))))) (_::_ merge (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (List a) (##_->_ (List b) (List (Pair a b))))))) (_::_ map-fst (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (List (Pair a b)) (List a))))) (_::_ map-snd (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (List (Pair a b)) (List b))))) (_::_ empty? (##_≡>_ (_:_ a Type) (##_->_ (List a) Bool))) (_::_ sort (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a (##_->_ a Bool)) (##_->_ (List a) (List a))))) (_::_ sfind (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a (##_->_ a Bool)) (##_->_ (##_->_ a Bool) (##_->_ a (##_->_ (List a) (Option a))))))) (_::_ sall (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a Bool) (##_->_ (List a) (List a))))) (_::_ sexist? (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a (##_->_ a Bool)) (##_->_ (##_->_ a Bool) (##_->_ a (##_->_ (List a) Bool)))))) (_::_ sinsert (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a (##_->_ a Bool)) (##_->_ a (##_->_ (List a) (List a)))))) (_::_ ssup (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a (##_->_ a Bool)) (##_->_ a (##_->_ (List a) (List a)))))) (_::_ sinf (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a (##_->_ a Bool)) (##_->_ a (##_->_ (List a) (List a)))))) (_::_ List->Array (##_≡>_ (_:_ a Type) (##_->_ (List a) (Array a))))))
+
+ |   do-lib       | 
+[35mtypecons[0m (record)   (cons Sexp[32m[249][0m (Sexp[32m[250][0m -> Sexp[32m[251][0m) (Sexp[32m[251][0m -> Sexp[32m[252][0m) (Elab_Context[32m[261][0m -> ((List[32m[159][0m ##TypeLevel.z Sexp[32m[253][0m) -> (List[32m[160][0m ##TypeLevel.z Sexp[32m[254][0m))) (String[32m[250][0m -> (String[32m[251][0m -> ((Option[32m[106][0m ##TypeLevel.z Sexp[32m[255][0m) -> ((List[32m[162][0m ##TypeLevel.z Sexp[32m[256][0m) -> Sexp[32m[257][0m)))) (bind_name : ##String) -> (return_name : ##String) -> (args : (List[32m[162][0m ##TypeLevel.z ##Sexp)) -> (IO[32m[261][0m ##Sexp) Macro[32m[152][0m Macro[32m[153][0m (str : ##String) -> (IO[32m[262][0m Unit[32m[225][0m) (a : (##Type_ ##TypeLevel.z)) ≡> (v : a[32m[0][0m) -> (IO[32m[264][0m a[32m[1][0m) (IO[32m[263][0m Unit[32m[226][0m) (IO[32m[264][0m Unit[32m[227][0m) (v : ##Float) -> (IO[32m[266][0m ##String))
+
+(##typecons (record) (cons (_::_ assign Sexp) (_::_ get-sym (##_->_ Sexp Sexp)) (_::_ get-op (##_->_ Sexp Sexp)) (_::_ get-decl (##_->_ Elab_Context (##_->_ (List Sexp) (List Sexp)))) (_::_ set-fun (##_->_ String (##_->_ String (##_->_ (Option Sexp) (##_->_ (List Sexp) Sexp))))) (_::_ do-impl (##_->_ (_:_ bind_name ##String) (##_->_ (_:_ return_name ##String) (##_->_ (_:_ args (List ##Sexp)) (IO ##Sexp))))) (_::_ do Macro) (_::_ do* Macro) (_::_ print (##_->_ (_:_ str ##String) (IO Unit))) (_::_ return (##_≡>_ (_:_ a (##Type_ ##TypeLevel_z)) (##_->_ (_:_ v a) (IO a)))) (_::_ newline (IO Unit)) (_::_ tab (IO Unit)) (_::_ float2string (##_->_ (_:_ v ##Float) (IO ##String)))))
+
+ |   do-impl      | 
+(bind_name : ##String) -> (return_name : ##String) -> (args : (List[32m[157][0m ##TypeLevel.z ##Sexp)) -> (IO[32m[256][0m ##Sexp)
+
+(##_->_ (_:_ bind_name ##String) (##_->_ (_:_ return_name ##String) (##_->_ (_:_ args (List ##Sexp)) (IO ##Sexp))))
+
+ |   do           | 
+Macro[32m[146][0m
+
+Macro
+
+ |   do*          | 
+Macro[32m[146][0m
+
+Macro
+
+ |   tuple-lib    | 
+[35mtypecons[0m (record)   (cons (a : (##Type_ ##TypeLevel.z)) ≡> ((List[32m[156][0m ##TypeLevel.z (IO[32m[254][0m a[32m[0][0m)) -> (IO[32m[255][0m (List[32m[157][0m ##TypeLevel.z a[32m[1][0m))) ((List[32m[156][0m ##TypeLevel.z Sexp[32m[250][0m) -> (IO[32m[255][0m (List[32m[157][0m ##TypeLevel.z Sexp[32m[251][0m))) ((List[32m[157][0m ##TypeLevel.z Sexp[32m[251][0m) -> (List[32m[158][0m ##TypeLevel.z Sexp[32m[252][0m)) ((List[32m[158][0m ##TypeLevel.z Sexp[32m[252][0m) -> (List[32m[159][0m ##TypeLevel.z Sexp[32m[253][0m)) Macro[32m[150][0m Macro[32m[151][0m ((List[32m[161][0m ##TypeLevel.z Sexp[32m[255][0m) -> ((List[32m[162][0m ##TypeLevel.z Sexp[32m[256][0m) -> (Sexp[32m[257][0m -> Sexp[32m[258][0m))) ((List[32m[162][0m ##TypeLevel.z Sexp[32m[256][0m) -> (IO[32m[261][0m Sexp[32m[257][0m)) Macro[32m[154][0m Macro[32m[155][0m)
+
+(##typecons (record) (cons (_::_ io-list (##_≡>_ (_:_ a (##Type_ ##TypeLevel_z)) (##_->_ (List (IO a)) (IO (List a))))) (_::_ gen-vars (##_->_ (List Sexp) (IO (List Sexp)))) (_::_ gen-tuple-names (##_->_ (List Sexp) (List Sexp))) (_::_ gen-deduce (##_->_ (List Sexp) (List Sexp))) (_::_ tuple-nth Macro) (_::_ assign-tuple Macro) (_::_ wrap-vars (##_->_ (List Sexp) (##_->_ (List Sexp) (##_->_ Sexp Sexp)))) (_::_ make-tuple-impl (##_->_ (List Sexp) (IO Sexp))) (_::_ make-tuple Macro) (_::_ tuple-type Macro)))
+
+ |   tuple-nth    | 
+Macro[32m[146][0m
+
+Macro
+
+ |   _<-_         | 
+Macro[32m[146][0m
+
+Macro
+
+ |   _,_          | 
+Macro[32m[146][0m
+
+Macro
+
+ |   Tuple        | 
+Macro[32m[146][0m
+
+Macro
+
+ |   case_        | 
+Macro[32m[146][0m
+
+Macro
+
+ |   plain-let…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   _|_          | 
+Macro[32m[146][0m
+
+Macro
+
+ |   depelim      | 
+[35mtypecons[0m (record)   (cons (args : (List[32m[155][0m ##TypeLevel.z ##Sexp)) -> (IO[32m[254][0m ##Sexp) Macro[32m[147][0m Macro[32m[148][0m)
+
+(##typecons (record) (cons (_::_ case_as_return_impl (##_->_ (_:_ args (List ##Sexp)) (IO ##Sexp))) (_::_ case_as_return_ Macro) (_::_ case_return_ Macro)))
+
+ |   case_as_r…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   case_retu…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   Test_file    | 
+Macro[32m[146][0m
+
+Macro
+
+    ============================================================================
+    ============================== LEXP CONTEXT : ==============================
+    =============================== Proba = 1/3 ===============================
+    =============================== Popu = 500 ===============================
+    | NAME       | LEXP_UNPARSE |  TYPE                                      | 
+    ----------------------------------------------------------------------------
+ |   Option       | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) -> (##Type_ ℓ[32m[1][0m)
+
+(##_≡>_ (_:_ ℓ TypeLevel) (##_->_ (_:_ a (##Type_ ℓ)) (##Type_ ℓ)))
+
+ |   some         | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (a[32m[0][0m -> (Option[32m[103][0m ℓ[32m[2][0m a[32m[1][0m))
+
+(##_->_ ?a (Option ?a))
+
+ |   none         | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (Option[32m[102][0m ℓ[32m[1][0m a[32m[0][0m)
+
+(##_≡>_ (_:_ ℓ TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (Option a)))
+
+ |   optionally   | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[1][0m)) ≡> (b : (##Type_ ℓ[32m[1][0m)) ≡> ((a[32m[1][0m -> b[32m[1][0m) -> (b[32m[1][0m -> ((Option[32m[106][0m ℓ[32m[5][0m a[32m[3][0m) -> b[32m[3][0m)))
+
+(##_->_ (##_->_ ?a ?b) (##_->_ ?b (##_->_ (Option ?a) ?b)))
+
+ |   List_leng…   | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> ((List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m) -> Int[32m[255][0m)
+
+(##_->_ (List ?a) Int)
+
+ |   List_head1   | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (xs : (List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m)) -> (Option[32m[103][0m ℓ[32m[2][0m a[32m[1][0m)
+
+(##_≡>_ (_:_ ℓ TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (_:_ xs (List a)) (Option a))))
+
+ |   List_head    | 
+(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ[32m[0][0m)) ≡> (x : τ[32m[0][0m) -> (xs : (List[32m[158][0m ℓ[32m[2][0m τ[32m[1][0m)) -> τ[32m[2][0m
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ τ (##Type_ ℓ)) (##_->_ (_:_ x τ) (##_->_ (_:_ xs (List τ)) τ))))
+
+ |   List_tail    | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (xs : (List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m)) -> (List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m)
+
+(##_≡>_ (_:_ ℓ TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (_:_ xs (List a)) (List a))))
+
+ |   List_map     | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[1][0m)) ≡> (b : (##Type_ ℓ[32m[1][0m)) ≡> ((a[32m[1][0m -> b[32m[1][0m) -> ((List[32m[160][0m ℓ[32m[4][0m a[32m[2][0m) -> (List[32m[161][0m ℓ[32m[4][0m b[32m[2][0m)))
+
+(##_->_ (##_->_ ?a ?b) (##_->_ (List ?a) (List ?b)))
+
+ |   List_foldr   | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (b : (##Type_ ℓ[32m[1][0m)) ≡> (a : (##Type_ ℓ[32m[1][0m)) ≡> ((b[32m[1][0m -> (a[32m[1][0m -> a[32m[2][0m)) -> ((List[32m[160][0m ℓ[32m[4][0m b[32m[2][0m) -> (a[32m[2][0m -> a[32m[3][0m)))
+
+(##_->_ (##_->_ ?b (##_->_ ?a ?a)) (##_->_ (List ?b) (##_->_ ?a ?a)))
+
+ |   List_find    | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> ((a[32m[0][0m -> Bool[32m[211][0m) -> ((List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m) -> (Option[32m[104][0m ℓ[32m[3][0m a[32m[2][0m)))
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (##_->_ a Bool) (##_->_ (List a) (Option a)))))
+
+ |   List_nth     | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (Int[32m[254][0m -> ((List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m) -> (a[32m[2][0m -> a[32m[3][0m)))
+
+(##_->_ Int (##_->_ (List ?a) (##_->_ ?a ?a)))
+
+ |   Sexp_error   | 
+Sexp[32m[249][0m
+
+Sexp
+
+ |   Sexp_to_l…   | 
+(s : ##Sexp) -> (exceptions : (List[32m[156][0m ##TypeLevel.z ##Sexp)) -> (List[32m[157][0m ##TypeLevel.z ##Sexp)
+
+(##_->_ (_:_ s ##Sexp) (##_->_ (_:_ exceptions (List ##Sexp)) (List ##Sexp)))
+
+ |   multiarg_…   | 
+(name : ##String) -> (margs : (List[32m[156][0m ##TypeLevel.z Sexp[32m[250][0m)) -> (IO[32m[255][0m ##Sexp)
+
+(##_->_ (_:_ name ##String) (##_->_ (_:_ margs (List Sexp)) (IO ##Sexp)))
+
+ |   lambda_->_   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   lambda_=>_   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   lambda_…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   List_reve…   | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> ((List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m) -> ((List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m) -> (List[32m[159][0m ℓ[32m[3][0m a[32m[2][0m)))
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (List a) (##_->_ (List a) (List a)))))
+
+ |   List_conc…   | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (l : (List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m)) -> (t : (List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m)) -> (List[32m[159][0m ℓ[32m[3][0m a[32m[2][0m)
+
+(##_->_ (_:_ l (List ?a)) (##_->_ (_:_ t (List ?a)) (List ?a)))
+
+ |   List_foldl   | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[1][0m)) ≡> (b : (##Type_ ℓ[32m[1][0m)) ≡> ((a[32m[1][0m -> (b[32m[1][0m -> a[32m[3][0m)) -> (a[32m[2][0m -> ((List[32m[161][0m ℓ[32m[4][0m b[32m[2][0m) -> a[32m[4][0m)))
+
+(##_->_ (##_->_ ?a (##_->_ ?b ?a)) (##_->_ ?a (##_->_ (List ?b) ?a)))
+
+ |   List_mapi    | 
+(a : Type[32m[245][0m) ≡> (b : Type[32m[246][0m) ≡> ((a[32m[1][0m -> (Int[32m[255][0m -> b[32m[2][0m)) -> ((List[32m[158][0m ##TypeLevel.z a[32m[2][0m) -> (List[32m[159][0m ##TypeLevel.z b[32m[2][0m)))
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (##_->_ a (##_->_ Int b)) (##_->_ (List a) (List b)))))
+
+ |   List_map2    | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[2][0m)) ≡> (b : (##Type_ ℓ[32m[2][0m)) ≡> (c : (##Type_ ℓ[32m[2][0m)) ≡> ((a[32m[2][0m -> (b[32m[2][0m -> c[32m[2][0m)) -> ((List[32m[162][0m ℓ[32m[6][0m a[32m[3][0m) -> ((List[32m[163][0m ℓ[32m[6][0m b[32m[3][0m) -> (List[32m[164][0m ℓ[32m[6][0m c[32m[3][0m))))
+
+(##_->_ (##_->_ ?a (##_->_ ?b ?c)) (##_->_ (List ?a) (##_->_ (List ?b) (List ?c))))
+
+ |   List_fold2   | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[2][0m)) ≡> (b : (##Type_ ℓ[32m[2][0m)) ≡> (c : (##Type_ ℓ[32m[2][0m)) ≡> ((a[32m[2][0m -> (b[32m[2][0m -> (c[32m[2][0m -> a[32m[5][0m))) -> (a[32m[3][0m -> ((List[32m[163][0m ℓ[32m[6][0m b[32m[3][0m) -> ((List[32m[164][0m ℓ[32m[6][0m c[32m[3][0m) -> a[32m[6][0m))))
+
+(##_->_ (##_->_ ?a (##_->_ ?b (##_->_ ?c ?a))) (##_->_ ?a (##_->_ (List ?b) (##_->_ (List ?c) ?a))))
+
+ |   List_empty   | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> ((List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m) -> Bool[32m[211][0m)
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (List a) Bool)))
+
+ |   I            | 
+(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ[32m[0][0m)) ≡> (x : τ[32m[0][0m) -> τ[32m[1][0m
+
+(##_->_ (_:_ x ?τ) ?τ)
+
+ |   K            | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (a[32m[0][0m -> (b : Type[32m[248][0m) ≡> (b[32m[0][0m -> a[32m[3][0m))
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ a (##_≡>_ (_:_ b Type) (##_->_ b a)))))
+
+ |   quote1       | 
+(Sexp[32m[249][0m -> Sexp[32m[250][0m)
+
+(##_->_ Sexp Sexp)
+
+ |   quote        | 
+Macro[32m[146][0m
+
+Macro
+
+ |   make-decl    | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> Sexp[32m[251][0m))
+
+(##_->_ Sexp (##_->_ Sexp Sexp))
+
+ |   chain-decl   | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> Sexp[32m[251][0m))
+
+(##_->_ Sexp (##_->_ Sexp Sexp))
+
+ |   chain-dec…   | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> (Sexp[32m[251][0m -> Sexp[32m[252][0m)))
+
+(##_->_ Sexp (##_->_ Sexp (##_->_ Sexp Sexp)))
+
+ |   make-cons    | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> Sexp[32m[251][0m))
+
+(##_->_ Sexp (##_->_ Sexp Sexp))
+
+ |   make-ann     | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> Sexp[32m[251][0m))
+
+(##_->_ Sexp (##_->_ Sexp Sexp))
+
+ |   type-impl    | 
+(x : (List[32m[155][0m ##TypeLevel.z Sexp[32m[249][0m)) -> (IO[32m[254][0m ##Sexp)
+
+(##_->_ (_:_ x (List Sexp)) (IO ##Sexp))
+
+ |   type_        | 
+Macro[32m[146][0m
+
+Macro
+
+ |   Sexp_wrap…   | 
+Type[32m[245][0m
+
+Type
+
+ |   node         | 
+(Sexp[32m[249][0m -> ((List[32m[156][0m ##TypeLevel.z Sexp[32m[250][0m) -> Sexp_wrapper[32m[66][0m))
+
+(##_->_ Sexp (##_->_ (List Sexp) Sexp_wrapper))
+
+ |   symbol       | 
+(String[32m[246][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ String Sexp_wrapper)
+
+ |   string       | 
+(String[32m[246][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ String Sexp_wrapper)
+
+ |   integer      | 
+(Integer[32m[251][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ Integer Sexp_wrapper)
+
+ |   float        | 
+(Float[32m[254][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ Float Sexp_wrapper)
+
+ |   block        | 
+(Sexp[32m[249][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ Sexp Sexp_wrapper)
+
+ |   Sexp_wrap    | 
+(s : ##Sexp) -> [35mtypecons[0m (Sexp_wrapper)   (block Sexp[32m[250][0m) (float Float[32m[255][0m) (integer Integer[32m[252][0m) (node Sexp[32m[250][0m (List[32m[157][0m ##TypeLevel.z Sexp[32m[251][0m)) (string String[32m[247][0m) (symbol String[32m[247][0m)
+
+(##_->_ (_:_ s ##Sexp) (##typecons (Sexp_wrapper) (block Sexp) (float Float) (integer Integer) (node Sexp (List Sexp)) (string String) (symbol String)))
+
+ |   BoolMod      | 
+([35mlambda [0m(t1 : (##Type_ (##TypeLevel.succ ##TypeLevel.z))) -> [35mlambda [0m(t2 : (##Type_ ##TypeLevel.z)) -> [35mlambda [0m(t3 : (##Type_ ##TypeLevel.z)) -> [35mtypecons[0m (_)   (cons t1[32m[2][0m t2[32m[2][0m t3[32m[2][0m) (##Type_ ##TypeLevel.z) [35mtypecons[0m (Bool)   (false) (true) [35mtypecons[0m (Bool)   (false) (true))
+
+((##lambda_->_ (_:_ t1 (##Type_ (##TypeLevel.succ ##TypeLevel_z))) (##lambda_->_ (_:_ t2 (##Type_ ##TypeLevel_z)) (##lambda_->_ (_:_ t3 (##Type_ ##TypeLevel_z)) (##typecons (_) (cons (_::_ t t1) (_::_ true t2) (_::_ false t3)))))) (##Type_ ##TypeLevel_z) (typecons Bool true false) (typecons Bool true false))
+
+ |   Pair         | 
+(a : Type[32m[245][0m) -> (b : Type[32m[246][0m) -> (##Type_ ##TypeLevel.z)
+
+(##_->_ (_:_ a Type) (##_->_ (_:_ b Type) (##Type_ ##TypeLevel_z)))
+
+ |   pair         | 
+(a : Type[32m[245][0m) ≡> (b : Type[32m[246][0m) ≡> (fst : a[32m[1][0m) -> (snd : b[32m[1][0m) -> (Pair[32m[59][0m a[32m[3][0m b[32m[2][0m)
+
+(##_->_ (_:_ fst ?a) (##_->_ (_:_ snd ?b) (Pair ?a ?b)))
+
+ |   Triplet      | 
+(a : Type[32m[245][0m) -> (b : Type[32m[246][0m) -> (c : Type[32m[247][0m) -> Type[32m[248][0m
+
+(##_->_ (_:_ a Type) (##_->_ (_:_ b Type) (##_->_ (_:_ c Type) Type)))
+
+ |   triplet      | 
+(a : Type[32m[245][0m) ≡> (b : Type[32m[246][0m) ≡> (c : Type[32m[247][0m) ≡> (x : a[32m[2][0m) -> (y : b[32m[2][0m) -> (z : c[32m[2][0m) -> (Triplet[32m[59][0m a[32m[5][0m b[32m[4][0m c[32m[3][0m)
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_≡>_ (_:_ c Type) (##_->_ (_:_ x a) (##_->_ (_:_ y b) (##_->_ (_:_ z c) (Triplet a b c)))))))
+
+ |   List_merge   | 
+(a : (##Type_ ##TypeLevel.z)) ≡> (b : (##Type_ ##TypeLevel.z)) ≡> ((List[32m[157][0m ##TypeLevel.z a[32m[1][0m) -> ((List[32m[158][0m ##TypeLevel.z b[32m[1][0m) -> (List[32m[159][0m ##TypeLevel.z (Pair[32m[59][0m a[32m[3][0m b[32m[2][0m))))
+
+(##_->_ (List ?a) (##_->_ (List ?b) (List (Pair ?a ?b))))
+
+ |   List_map-…   | 
+(τ : (##Type_ ##TypeLevel.z)) ≡> (b : Type[32m[246][0m) ≡> (xs : (List[32m[157][0m ##TypeLevel.z (Pair[32m[57][0m τ[32m[1][0m b[32m[0][0m))) -> (List[32m[158][0m ##TypeLevel.z τ[32m[2][0m)
+
+(##_≡>_ (_:_ τ (##Type_ ##TypeLevel_z)) (##_≡>_ (_:_ b Type) (##_->_ (_:_ xs (List (Pair τ b))) (List τ))))
+
+ |   List_map-…   | 
+(a : Type[32m[245][0m) ≡> (τ : (##Type_ ##TypeLevel.z)) ≡> (xs : (List[32m[157][0m ##TypeLevel.z (Pair[32m[57][0m a[32m[1][0m τ[32m[0][0m))) -> (List[32m[158][0m ##TypeLevel.z τ[32m[1][0m)
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ τ (##Type_ ##TypeLevel_z)) (##_->_ (_:_ xs (List (Pair a τ))) (List τ))))
+
+ |   False        | 
+(##Type_ ##TypeLevel.z)
+
+(##Type_ ##TypeLevel_z)
+
+ |   True         | 
+(##Type_ ##TypeLevel.z)
+
+(##Type_ ##TypeLevel_z)
+
+ |   Not          | 
+(ℓ : ##TypeLevel) ≡> (prop : (##Type_ ℓ[32m[0][0m)) -> (##Type_ ℓ[32m[1][0m)
+
+(##_->_ (_:_ prop (##Type_ ?ℓ)) (##Type_ ?ℓ))
+
+ |   Decidable    | 
+(ℓ : ##TypeLevel) => (prop : (##Type_ ℓ[32m[0][0m)) -> (##Type_ ℓ[32m[1][0m)
+
+(##_=>_ (_:_ ℓ ##TypeLevel) (##_->_ (_:_ prop (##Type_ ℓ)) (##Type_ ℓ)))
+
+ |   LList        | 
+(Type[32m[245][0m -> (Int[32m[253][0m -> Type[32m[247][0m))
+
+(##_->_ Type (##_->_ Int Type))
+
+ |   vnil         | 
+(a : Type[32m[245][0m) ≡> (n : Int[32m[253][0m) ≡> (p : (Eq[32m[259][0m ##TypeLevel.z ##Int n[32m[0][0m (Integer->Int[32m[185][0m [33m0[0m))) ≡> (LList[32m[47][0m a[32m[2][0m n[32m[1][0m)
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ n Int) (##_≡>_ (_:_ p (Eq n (Integer->Int (##typer-immediate 0)))) (LList a n))))
+
+ |   vcons        | 
+(a : Type[32m[245][0m) ≡> (n : Int[32m[253][0m) ≡> (n1 : Int[32m[254][0m) ≡> (a[32m[2][0m -> ((LList[32m[48][0m a[32m[3][0m n1[32m[1][0m) -> (p : (Eq[32m[262][0m ##TypeLevel.z ##Int n[32m[3][0m (Int_+[32m[210][0m n1[32m[2][0m (Integer->Int[32m[188][0m [33m1[0m)))) ≡> (LList[32m[50][0m a[32m[5][0m n[32m[4][0m)))
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ n Int) (##_≡>_ (_:_ n1 Int) (##_->_ a (##_->_ (LList a n1) (##_≡>_ (_:_ p (Eq n (Int_+ n1 (Integer->Int (##typer-immediate 1))))) (LList a n)))))))
+
+ |   if_then_e…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   not          | 
+(Bool[32m[208][0m -> Bool[32m[209][0m)
+
+(##_->_ Bool Bool)
+
+ |   or           | 
+(Bool[32m[208][0m -> (Bool[32m[209][0m -> Bool[32m[210][0m))
+
+(##_->_ Bool (##_->_ Bool Bool))
+
+ |   and          | 
+(Bool[32m[208][0m -> (Bool[32m[209][0m -> Bool[32m[210][0m))
+
+(##_->_ Bool (##_->_ Bool Bool))
+
+ |   xor          | 
+(Bool[32m[208][0m -> (Bool[32m[209][0m -> Bool[32m[210][0m))
+
+(##_->_ Bool (##_->_ Bool Bool))
+
+ |   fold         | 
+(Bool[32m[208][0m -> (a : Type[32m[246][0m) ≡> (a[32m[0][0m -> (a[32m[1][0m -> a[32m[2][0m)))
+
+(##_->_ Bool (##_≡>_ (_:_ a Type) (##_->_ a (##_->_ a a))))
+
+ |   test1        | 
+(Option[32m[100][0m ##TypeLevel.z Int[32m[252][0m)
+
+(Option Int)
+
+ |   test2        | 
+(Option[32m[100][0m ##TypeLevel.z Int[32m[252][0m)
+
+(Option Int)
+
+ |   test3        | 
+(Option[32m[100][0m ##TypeLevel.z Int[32m[252][0m)
+
+(Option Int)
+
+ |   test4        | 
+(Option[32m[100][0m ##TypeLevel.z Int[32m[252][0m)
+
+(Option Int)
+
+ |   Elab_nth-…   | 
+(a : ##String) -> (b : ##Int) -> (c : ##Elab_Context) -> (Option[32m[103][0m ##TypeLevel.z ##String)
+
+(##_->_ (_:_ a ##String) (##_->_ (_:_ b ##Int) (##_->_ (_:_ c ##Elab_Context) (Option ##String))))
+
+ |   Elab_arg-…   | 
+(a : ##String) -> (b : ##String) -> (c : ##Elab_Context) -> (Option[32m[103][0m ##TypeLevel.z ##Int)
+
+(##_->_ (_:_ a ##String) (##_->_ (_:_ b ##String) (##_->_ (_:_ c ##Elab_Context) (Option ##Int))))
+
+ |   poly-lits    | 
+[35mtypecons[0m (record)   (cons (α : Type[32m[245][0m) -> Type[32m[246][0m (α : Type[32m[246][0m) ≡> (fromInteger : (Integer[32m[253][0m -> α[32m[1][0m)) -> ([35mlet [0mFromInteger : (α : Type[32m[248][0m) -> Type[32m[249][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[249][0m))  (mkFromInteger (Integer[32m[256][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[249][0m))  (mkFromInteger (Integer[32m[256][0m -> α[32m[1][0m)) α[32m[1][0m) (α : Type[32m[247][0m) ≡> (inst : ([35mlet [0mFromInteger : (α : Type[32m[248][0m) -> Type[32m[249][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[249][0m))  (mkFromInteger (Integer[32m[256][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[249][0m))  (mkFromInteger (Integer[32m[256][0m -> α[32m[1][0m)) α[32m[0][0m)) => (Integer[32m[255][0m -> α[32m[2][0m) Macro[32m[149][0m ([35mlet [0mFromInteger : (α : Type[32m[249][0m) -> Type[32m[250][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[250][0m))  (mkFromInteger (Integer[32m[257][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[250][0m))  (mkFromInteger (Integer[32m[257][0m -> α[32m[1][0m)) Integer[32m[255][0m) ([35mlet [0mFromInteger : (α : Type[32m[250][0m) -> Type[32m[251][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[251][0m))  (mkFromInteger (Integer[32m[258][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[251][0m))  (mkFromInteger (Integer[32m[258][0m -> α[32m[1][0m)) Int[32m[257][0m))
+
+(##typecons (record) (cons (_::_ FromInteger (##_->_ (_:_ α Type) Type)) (_::_ mkFromInteger (##_≡>_ (_:_ α Type) (##_->_ (_:_ fromInteger (##_->_ Integer α)) ((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) α)))) (_::_ fromInteger (##_≡>_ (_:_ α Type) (##_=>_ (_:_ inst ((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) α)) (##_->_ Integer α)))) (_::_ typer-immediate Macro) (_::_ IntegerFromInteger ((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) Integer)) (_::_ IntFromInteger ((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) Int))))
+
+ |   typer-imm…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   FromInteg…   | 
+(α : Type[32m[245][0m) -> Type[32m[246][0m
+
+(##_->_ (_:_ α Type) Type)
+
+ |   mkFromInt…   | 
+(α : Type[32m[245][0m) ≡> (fromInteger : (Integer[32m[252][0m -> α[32m[1][0m)) -> ([35mlet [0mFromInteger : (α : Type[32m[247][0m) -> Type[32m[248][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[248][0m))  (mkFromInteger (Integer[32m[255][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[248][0m))  (mkFromInteger (Integer[32m[255][0m -> α[32m[1][0m)) α[32m[1][0m)
+
+(##_->_ (_:_ fromInteger (##_->_ Integer ?α)) ((##let_in_ (_;_ (_:_ FromInteger (_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) ?α))
+
+ |   fromInteg…   | 
+(α : Type[32m[245][0m) ≡> (inst : ([35mlet [0mFromInteger : (α : Type[32m[246][0m) -> Type[32m[247][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[247][0m))  (mkFromInteger (Integer[32m[254][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[247][0m))  (mkFromInteger (Integer[32m[254][0m -> α[32m[1][0m)) α[32m[0][0m)) => (Integer[32m[253][0m -> α[32m[2][0m)
+
+(##_≡>_ (_:_ α Type) (##_=>_ (_:_ inst ((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) α)) (##_->_ Integer α)))
+
+ |   IntFromIn…   | 
+([35mlet [0mFromInteger : (α : Type[32m[245][0m) -> Type[32m[246][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[246][0m))  (mkFromInteger (Integer[32m[253][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[246][0m))  (mkFromInteger (Integer[32m[253][0m -> α[32m[1][0m)) Int[32m[252][0m)
+
+((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) Int)
+
+ |   IntegerFr…   | 
+([35mlet [0mFromInteger : (α : Type[32m[245][0m) -> Type[32m[246][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[246][0m))  (mkFromInteger (Integer[32m[253][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[246][0m))  (mkFromInteger (Integer[32m[253][0m -> α[32m[1][0m)) Integer[32m[251][0m)
+
+((##let_in_ (_;_ (_:_ FromInteger (_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) Integer)
+
+ |   monads       | 
+[35mtypecons[0m (record)   (cons (M : (Type[32m[245][0m -> Type[32m[246][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)) (M : (Type[32m[246][0m -> Type[32m[247][0m)) ≡> (bind : (a : Type[32m[247][0m) ≡> (b : Type[32m[248][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m)))) -> (pure : (a : Type[32m[248][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) -> ([35mlet [0mMonad : (M : (Type[32m[249][0m -> Type[32m[250][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) M[32m[2][0m) (M : (Type[32m[247][0m -> Type[32m[248][0m)) ≡> (monad : ([35mlet [0mMonad : (M : (Type[32m[248][0m -> Type[32m[249][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[249][0m -> Type[32m[250][0m)))  (mkMonad (a : Type[32m[250][0m) ≡> (b : Type[32m[251][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[251][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[249][0m -> Type[32m[250][0m)))  (mkMonad (a : Type[32m[250][0m) ≡> (b : Type[32m[251][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[251][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) M[32m[0][0m)) => (a : Type[32m[249][0m) ≡> (b : Type[32m[250][0m) ≡> ((M[32m[3][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[5][0m b[32m[2][0m)) -> (M[32m[5][0m b[32m[2][0m))) (M : (Type[32m[248][0m -> Type[32m[249][0m)) ≡> (monad : ([35mlet [0mMonad : (M : (Type[32m[249][0m -> Type[32m[250][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) M[32m[0][0m)) => (a : Type[32m[250][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)) ([35mlet [0mMonad : (M : (Type[32m[249][0m -> Type[32m[250][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) IO[32m[257][0m) (a : Type[32m[250][0m) ≡> (b : Type[32m[251][0m) ≡> ((Option[32m[107][0m ##TypeLevel.z a[32m[1][0m) -> ((a[32m[2][0m -> (Option[32m[109][0m ##TypeLevel.z b[32m[2][0m)) -> (Option[32m[109][0m ##TypeLevel.z b[32m[2][0m))) (a : Type[32m[251][0m) ≡> (a[32m[0][0m -> (Option[32m[108][0m ##TypeLevel.z a[32m[1][0m)) ([35mlet [0mMonad : (M : (Type[32m[252][0m -> Type[32m[253][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[253][0m -> Type[32m[254][0m)))  (mkMonad (a : Type[32m[254][0m) ≡> (b : Type[32m[255][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[255][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[253][0m -> Type[32m[254][0m)))  (mkMonad (a : Type[32m[254][0m) ≡> (b : Type[32m[255][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[255][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) (Option[32m[107][0m ##TypeLevel.z)))
+ crossover --> (##typecons (record) (cons (_::_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_::_ mkMonad (##_≡>_ (_:_ M (##_->_ Type Type)) (##_->_ (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (##_->_ (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))) ((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) M))))) (_::_ bind (##_≡>_ (_:_ M (##_->_ Type Type)) (##_=>_ (_:_ monad ((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) M)) (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))))) (_::_ pure (##_≡>_ (_:_ M (##_->_ Type Type)) (##_=>_ (_:_ monad ((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) M)) (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))) (_::_ IO_monad ((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) IO)) (_::_ Option_bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (Option a) (##_->_ (##_->_ a (Option b)) (Option b)))))) (_::_ Option_pure (##_≡>_ (_:_ a Type) (##_->_ a (Option a)))) (_::_ Option_monad ((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) (Option)))))
+
+ |   Monad        | 
+(M : (Type[32m[245][0m -> Type[32m[246][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z))
+ crossover --> (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))
+
+ |   bind         | 
+(M : (Type[32m[245][0m -> Type[32m[246][0m)) ≡> (monad : ([35mlet [0mMonad : (M : (Type[32m[246][0m -> Type[32m[247][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[247][0m -> Type[32m[248][0m)))  (mkMonad (a : Type[32m[248][0m) ≡> (b : Type[32m[249][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[249][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[247][0m -> Type[32m[248][0m)))  (mkMonad (a : Type[32m[248][0m) ≡> (b : Type[32m[249][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[249][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) M[32m[0][0m)) => (a : Type[32m[247][0m) ≡> (b : Type[32m[248][0m) ≡> ((M[32m[3][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[5][0m b[32m[2][0m)) -> (M[32m[5][0m b[32m[2][0m)))
+
+(##_≡>_ (_:_ M (##_->_ Type Type)) (##_=>_ (_:_ monad ((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) M)) (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))))
+
+ |   pure         | 
+(M : (Type[32m[245][0m -> Type[32m[246][0m)) ≡> (monad : ([35mlet [0mMonad : (M : (Type[32m[246][0m -> Type[32m[247][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[247][0m -> Type[32m[248][0m)))  (mkMonad (a : Type[32m[248][0m) ≡> (b : Type[32m[249][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[249][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[247][0m -> Type[32m[248][0m)))  (mkMonad (a : Type[32m[248][0m) ≡> (b : Type[32m[249][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[249][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) M[32m[0][0m)) => (a : Type[32m[247][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))
+
+(##_≡>_ (_:_ M (##_->_ Type Type)) (##_=>_ (_:_ monad ((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) M)) (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))
+
+ |   IO_monad     | 
+([35mlet [0mMonad : (M : (Type[32m[245][0m -> Type[32m[246][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[246][0m -> Type[32m[247][0m)))  (mkMonad (a : Type[32m[247][0m) ≡> (b : Type[32m[248][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[248][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[246][0m -> Type[32m[247][0m)))  (mkMonad (a : Type[32m[247][0m) ≡> (b : Type[32m[248][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[248][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) IO[32m[253][0m)
+
+((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (##_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (##_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) IO)
+
+ |   Option_mo…   | 
+([35mlet [0mMonad : (M : (Type[32m[245][0m -> Type[32m[246][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[246][0m -> Type[32m[247][0m)))  (mkMonad (a : Type[32m[247][0m) ≡> (b : Type[32m[248][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[248][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[246][0m -> Type[32m[247][0m)))  (mkMonad (a : Type[32m[247][0m) ≡> (b : Type[32m[248][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[248][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) (Option[32m[100][0m ##TypeLevel.z))
+
+((##let_in_ (_;_ (_:_ Monad (##_->_ (_:_ M (_->_ Type Type)) (##Type_ (##TypeLevel.succ ##TypeLevel_z)))) (_=_ Monad (##typecons (Monad (_:_ M (_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a)))))))) (##typecons (Monad (_:_ M (_->_ Type Type))) (mkMonad (_:_ bind (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (M a) (##_->_ (##_->_ a (M b)) (M b)))))) (_:_ pure (##_≡>_ (_:_ a Type) (##_->_ a (M a))))))) (Option))
+
+ |   list         | 
+[35mtypecons[0m (record)   (cons (a : Type[32m[245][0m) ≡> ((List[32m[156][0m ##TypeLevel.z a[32m[0][0m) -> Int[32m[254][0m) (a : Type[32m[246][0m) ≡> ((List[32m[157][0m ##TypeLevel.z a[32m[0][0m) -> (Option[32m[103][0m ##TypeLevel.z a[32m[1][0m)) (a : Type[32m[247][0m) ≡> ((List[32m[158][0m ##TypeLevel.z a[32m[0][0m) -> (Option[32m[104][0m ##TypeLevel.z a[32m[1][0m)) (a : Type[32m[248][0m) ≡> ((List[32m[159][0m ##TypeLevel.z a[32m[0][0m) -> (List[32m[160][0m ##TypeLevel.z a[32m[1][0m)) (a : Type[32m[249][0m) ≡> (b : Type[32m[250][0m) ≡> ((a[32m[1][0m -> b[32m[1][0m) -> ((List[32m[162][0m ##TypeLevel.z a[32m[2][0m) -> (List[32m[163][0m ##TypeLevel.z b[32m[2][0m))) (a : Type[32m[250][0m) ≡> (b : Type[32m[251][0m) ≡> ((a[32m[1][0m -> (Int[32m[260][0m -> b[32m[2][0m)) -> ((List[32m[163][0m ##TypeLevel.z a[32m[2][0m) -> (List[32m[164][0m ##TypeLevel.z b[32m[2][0m))) (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> (c : Type[32m[253][0m) ≡> ((a[32m[2][0m -> (b[32m[2][0m -> c[32m[2][0m)) -> ((List[32m[165][0m ##TypeLevel.z a[32m[3][0m) -> ((List[32m[166][0m ##TypeLevel.z b[32m[3][0m) -> (List[32m[167][0m ##TypeLevel.z c[32m[3][0m)))) (a : Type[32m[252][0m) ≡> (b : Type[32m[253][0m) ≡> ((a[32m[1][0m -> (b[32m[1][0m -> (Int[32m[263][0m -> a[32m[4][0m))) -> (a[32m[2][0m -> ((List[32m[166][0m ##TypeLevel.z b[32m[2][0m) -> a[32m[4][0m))) (a : Type[32m[253][0m) ≡> (b : Type[32m[254][0m) ≡> (c : Type[32m[255][0m) ≡> ((a[32m[2][0m -> (b[32m[2][0m -> (c[32m[2][0m -> a[32m[5][0m))) -> (a[32m[3][0m -> ((List[32m[168][0m ##TypeLevel.z b[32m[3][0m) -> ((List[32m[169][0m ##TypeLevel.z c[32m[3][0m) -> a[32m[6][0m)))) (a : Type[32m[254][0m) ≡> (b : Type[32m[255][0m) ≡> ((b[32m[0][0m -> (a[32m[2][0m -> a[32m[3][0m)) -> ((List[32m[167][0m ##TypeLevel.z b[32m[1][0m) -> (a[32m[3][0m -> a[32m[4][0m))) (a : Type[32m[255][0m) ≡> ((a[32m[0][0m -> Bool[32m[220][0m) -> ((List[32m[167][0m ##TypeLevel.z a[32m[1][0m) -> (Option[32m[113][0m ##TypeLevel.z a[32m[2][0m))) (a : Type[32m[256][0m) ≡> (Int[32m[264][0m -> ((List[32m[168][0m ##TypeLevel.z a[32m[1][0m) -> (a[32m[2][0m -> a[32m[3][0m))) (a : Type[32m[257][0m) ≡> ((List[32m[168][0m ##TypeLevel.z a[32m[0][0m) -> ((List[32m[169][0m ##TypeLevel.z a[32m[1][0m) -> (List[32m[170][0m ##TypeLevel.z a[32m[2][0m))) (a : Type[32m[258][0m) ≡> ((List[32m[169][0m ##TypeLevel.z a[32m[0][0m) -> ((List[32m[170][0m ##TypeLevel.z a[32m[1][0m) -> (List[32m[171][0m ##TypeLevel.z a[32m[2][0m))) (a : Type[32m[259][0m) ≡> (b : Type[32m[260][0m) ≡> ((a[32m[1][0m -> (b[32m[1][0m -> a[32m[3][0m)) -> (a[32m[2][0m -> ((List[32m[173][0m ##TypeLevel.z b[32m[2][0m) -> a[32m[4][0m))) (a : Type[32m[260][0m) ≡> ((a[32m[0][0m -> Bool[32m[225][0m) -> ((List[32m[172][0m ##TypeLevel.z a[32m[1][0m) -> (List[32m[173][0m ##TypeLevel.z a[32m[2][0m))) (a : Type[32m[261][0m) ≡> (b : Type[32m[262][0m) ≡> ((List[32m[173][0m ##TypeLevel.z a[32m[1][0m) -> ((List[32m[174][0m ##TypeLevel.z b[32m[1][0m) -> (List[32m[175][0m ##TypeLevel.z (Pair[32m[75][0m a[32m[3][0m b[32m[2][0m)))) (a : Type[32m[262][0m) ≡> (b : Type[32m[263][0m) ≡> ((List[32m[174][0m ##TypeLevel.z (Pair[32m[74][0m a[32m[1][0m b[32m[0][0m)) -> (List[32m[175][0m ##TypeLevel.z a[32m[2][0m)) (a : Type[32m[263][0m) ≡> (b : Type[32m[264][0m) ≡> ((List[32m[175][0m ##TypeLevel.z (Pair[32m[75][0m a[32m[1][0m b[32m[0][0m)) -> (List[32m[176][0m ##TypeLevel.z b[32m[1][0m)) (a : Type[32m[264][0m) ≡> ((List[32m[175][0m ##TypeLevel.z a[32m[0][0m) -> Bool[32m[229][0m) (a : Type[32m[265][0m) ≡> ((a[32m[0][0m -> (a[32m[1][0m -> Bool[32m[231][0m)) -> ((List[32m[177][0m ##TypeLevel.z a[32m[1][0m) -> (List[32m[178][0m ##TypeLevel.z a[32m[2][0m))) (a : Type[32m[266][0m) ≡> ((a[32m[0][0m -> (a[32m[1][0m -> Bool[32m[232][0m)) -> ((a[32m[1][0m -> Bool[32m[232][0m) -> (a[32m[2][0m -> ((List[32m[180][0m ##TypeLevel.z a[32m[3][0m) -> (Option[32m[126][0m ##TypeLevel.z a[32m[4][0m))))) (a : Type[32m[267][0m) ≡> ((a[32m[0][0m -> Bool[32m[232][0m) -> ((List[32m[179][0m ##TypeLevel.z a[32m[1][0m) -> (List[32m[180][0m ##TypeLevel.z a[32m[2][0m))) (a : Type[32m[268][0m) ≡> ((a[32m[0][0m -> (a[32m[1][0m -> Bool[32m[234][0m)) -> ((a[32m[1][0m -> Bool[32m[234][0m) -> (a[32m[2][0m -> ((List[32m[182][0m ##TypeLevel.z a[32m[3][0m) -> Bool[32m[236][0m)))) (a : Type[32m[269][0m) ≡> ((a[32m[0][0m -> (a[32m[1][0m -> Bool[32m[235][0m)) -> (a[32m[1][0m -> ((List[32m[182][0m ##TypeLevel.z a[32m[2][0m) -> (List[32m[183][0m ##TypeLevel.z a[32m[3][0m)))) (a : Type[32m[270][0m) ≡> ((a[32m[0][0m -> (a[32m[1][0m -> Bool[32m[236][0m)) -> (a[32m[1][0m -> ((List[32m[183][0m ##TypeLevel.z a[32m[2][0m) -> (List[32m[184][0m ##TypeLevel.z a[32m[3][0m)))) (a : Type[32m[271][0m) ≡> ((a[32m[0][0m -> (a[32m[1][0m -> Bool[32m[237][0m)) -> (a[32m[1][0m -> ((List[32m[184][0m ##TypeLevel.z a[32m[2][0m) -> (List[32m[185][0m ##TypeLevel.z a[32m[3][0m)))) (a : Type[32m[272][0m) ≡> ((List[32m[183][0m ##TypeLevel.z a[32m[0][0m) -> (Array[32m[290][0m a[32m[1][0m)))
+
+(##typecons (record) (cons (_::_ length (##_≡>_ (_:_ a Type) (##_->_ (List a) Int))) (_::_ head1 (##_≡>_ (_:_ a Type) (##_->_ (List a) (Option a)))) (_::_ head (##_≡>_ (_:_ a Type) (##_->_ (List a) (Option a)))) (_::_ tail (##_≡>_ (_:_ a Type) (##_->_ (List a) (List a)))) (_::_ map (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (##_->_ a b) (##_->_ (List a) (List b)))))) (_::_ mapi (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (##_->_ a (##_->_ Int b)) (##_->_ (List a) (List b)))))) (_::_ map2 (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_≡>_ (_:_ c Type) (##_->_ (##_->_ a (##_->_ b c)) (##_->_ (List a) (##_->_ (List b) (List c)))))))) (_::_ foldli (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (##_->_ a (##_->_ b (##_->_ Int a))) (##_->_ a (##_->_ (List b) a)))))) (_::_ fold2 (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_≡>_ (_:_ c Type) (##_->_ (##_->_ a (##_->_ b (##_->_ c a))) (##_->_ a (##_->_ (List b) (##_->_ (List c) a)))))))) (_::_ foldr (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (##_->_ b (##_->_ a a)) (##_->_ (List b) (##_->_ a a)))))) (_::_ find (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a Bool) (##_->_ (List a) (Option a))))) (_::_ nth (##_≡>_ (_:_ a Type) (##_->_ Int (##_->_ (List a) (##_->_ a a))))) (_::_ reverse (##_≡>_ (_:_ a Type) (##_->_ (List a) (##_->_ (List a) (List a))))) (_::_ concat (##_≡>_ (_:_ a Type) (##_->_ (List a) (##_->_ (List a) (List a))))) (_::_ foldl (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (##_->_ a (##_->_ b a)) (##_->_ a (##_->_ (List b) a)))))) (_::_ remove (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a Bool) (##_->_ (List a) (List a))))) (_::_ merge (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (List a) (##_->_ (List b) (List (Pair a b))))))) (_::_ map-fst (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (List (Pair a b)) (List a))))) (_::_ map-snd (##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (List (Pair a b)) (List b))))) (_::_ empty? (##_≡>_ (_:_ a Type) (##_->_ (List a) Bool))) (_::_ sort (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a (##_->_ a Bool)) (##_->_ (List a) (List a))))) (_::_ sfind (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a (##_->_ a Bool)) (##_->_ (##_->_ a Bool) (##_->_ a (##_->_ (List a) (Option a))))))) (_::_ sall (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a Bool) (##_->_ (List a) (List a))))) (_::_ sexist? (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a (##_->_ a Bool)) (##_->_ (##_->_ a Bool) (##_->_ a (##_->_ (List a) Bool)))))) (_::_ sinsert (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a (##_->_ a Bool)) (##_->_ a (##_->_ (List a) (List a)))))) (_::_ ssup (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a (##_->_ a Bool)) (##_->_ a (##_->_ (List a) (List a)))))) (_::_ sinf (##_≡>_ (_:_ a Type) (##_->_ (##_->_ a (##_->_ a Bool)) (##_->_ a (##_->_ (List a) (List a)))))) (_::_ List->Array (##_≡>_ (_:_ a Type) (##_->_ (List a) (Array a))))))
+
+ |   do-lib       | 
+[35mtypecons[0m (record)   (cons Sexp[32m[249][0m (Sexp[32m[250][0m -> Sexp[32m[251][0m) (Sexp[32m[251][0m -> Sexp[32m[252][0m) (Elab_Context[32m[261][0m -> ((List[32m[159][0m ##TypeLevel.z Sexp[32m[253][0m) -> (List[32m[160][0m ##TypeLevel.z Sexp[32m[254][0m))) (String[32m[250][0m -> (String[32m[251][0m -> ((Option[32m[106][0m ##TypeLevel.z Sexp[32m[255][0m) -> ((List[32m[162][0m ##TypeLevel.z Sexp[32m[256][0m) -> Sexp[32m[257][0m)))) (bind_name : ##String) -> (return_name : ##String) -> (args : (List[32m[162][0m ##TypeLevel.z ##Sexp)) -> (IO[32m[261][0m ##Sexp) Macro[32m[152][0m Macro[32m[153][0m (str : ##String) -> (IO[32m[262][0m Unit[32m[225][0m) (a : (##Type_ ##TypeLevel.z)) ≡> (v : a[32m[0][0m) -> (IO[32m[264][0m a[32m[1][0m) (IO[32m[263][0m Unit[32m[226][0m) (IO[32m[264][0m Unit[32m[227][0m) (v : ##Float) -> (IO[32m[266][0m ##String))
+
+(##typecons (record) (cons (_::_ assign Sexp) (_::_ get-sym (##_->_ Sexp Sexp)) (_::_ get-op (##_->_ Sexp Sexp)) (_::_ get-decl (##_->_ Elab_Context (##_->_ (List Sexp) (List Sexp)))) (_::_ set-fun (##_->_ String (##_->_ String (##_->_ (Option Sexp) (##_->_ (List Sexp) Sexp))))) (_::_ do-impl (##_->_ (_:_ bind_name ##String) (##_->_ (_:_ return_name ##String) (##_->_ (_:_ args (List ##Sexp)) (IO ##Sexp))))) (_::_ do Macro) (_::_ do* Macro) (_::_ print (##_->_ (_:_ str ##String) (IO Unit))) (_::_ return (##_≡>_ (_:_ a (##Type_ ##TypeLevel_z)) (##_->_ (_:_ v a) (IO a)))) (_::_ newline (IO Unit)) (_::_ tab (IO Unit)) (_::_ float2string (##_->_ (_:_ v ##Float) (IO ##String)))))
+
+ |   do-impl      | 
+(bind_name : ##String) -> (return_name : ##String) -> (args : (List[32m[157][0m ##TypeLevel.z ##Sexp)) -> (IO[32m[256][0m ##Sexp)
+
+(##_->_ (_:_ bind_name ##String) (##_->_ (_:_ return_name ##String) (##_->_ (_:_ args (List ##Sexp)) (IO ##Sexp))))
+
+ |   do           | 
+Macro[32m[146][0m
+
+Macro
+
+ |   do*          | 
+Macro[32m[146][0m
+
+Macro
+
+ |   tuple-lib    | 
+[35mtypecons[0m (record)   (cons (a : (##Type_ ##TypeLevel.z)) ≡> ((List[32m[156][0m ##TypeLevel.z (IO[32m[254][0m a[32m[0][0m)) -> (IO[32m[255][0m (List[32m[157][0m ##TypeLevel.z a[32m[1][0m))) ((List[32m[156][0m ##TypeLevel.z Sexp[32m[250][0m) -> (IO[32m[255][0m (List[32m[157][0m ##TypeLevel.z Sexp[32m[251][0m))) ((List[32m[157][0m ##TypeLevel.z Sexp[32m[251][0m) -> (List[32m[158][0m ##TypeLevel.z Sexp[32m[252][0m)) ((List[32m[158][0m ##TypeLevel.z Sexp[32m[252][0m) -> (List[32m[159][0m ##TypeLevel.z Sexp[32m[253][0m)) Macro[32m[150][0m Macro[32m[151][0m ((List[32m[161][0m ##TypeLevel.z Sexp[32m[255][0m) -> ((List[32m[162][0m ##TypeLevel.z Sexp[32m[256][0m) -> (Sexp[32m[257][0m -> Sexp[32m[258][0m))) ((List[32m[162][0m ##TypeLevel.z Sexp[32m[256][0m) -> (IO[32m[261][0m Sexp[32m[257][0m)) Macro[32m[154][0m Macro[32m[155][0m)
+
+(##typecons (record) (cons (_::_ io-list (##_≡>_ (_:_ a (##Type_ ##TypeLevel_z)) (##_->_ (List (IO a)) (IO (List a))))) (_::_ gen-vars (##_->_ (List Sexp) (IO (List Sexp)))) (_::_ gen-tuple-names (##_->_ (List Sexp) (List Sexp))) (_::_ gen-deduce (##_->_ (List Sexp) (List Sexp))) (_::_ tuple-nth Macro) (_::_ assign-tuple Macro) (_::_ wrap-vars (##_->_ (List Sexp) (##_->_ (List Sexp) (##_->_ Sexp Sexp)))) (_::_ make-tuple-impl (##_->_ (List Sexp) (IO Sexp))) (_::_ make-tuple Macro) (_::_ tuple-type Macro)))
+
+ |   tuple-nth    | 
+Macro[32m[146][0m
+
+Macro
+
+ |   _<-_         | 
+Macro[32m[146][0m
+
+Macro
+
+ |   _,_          | 
+Macro[32m[146][0m
+
+Macro
+
+ |   Tuple        | 
+Macro[32m[146][0m
+
+Macro
+
+ |   case_        | 
+Macro[32m[146][0m
+
+Macro
+
+ |   plain-let…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   _|_          | 
+Macro[32m[146][0m
+
+Macro
+
+ |   depelim      | 
+[35mtypecons[0m (record)   (cons (args : (List[32m[155][0m ##TypeLevel.z ##Sexp)) -> (IO[32m[254][0m ##Sexp) Macro[32m[147][0m Macro[32m[148][0m)
+
+(##typecons (record) (cons (_::_ case_as_return_impl (##_->_ (_:_ args (List ##Sexp)) (IO ##Sexp))) (_::_ case_as_return_ Macro) (_::_ case_return_ Macro)))
+
+ |   case_as_r…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   case_retu…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   Test_file    | 
+Macro[32m[146][0m
+
+Macro
+
+    ============================================================================
+    ============================== LEXP CONTEXT : ==============================
+    =============================== Proba = 1/4 ===============================
+    =============================== Popu = 500 ===============================
+    | NAME       | LEXP_UNPARSE |  TYPE                                      | 
+    ----------------------------------------------------------------------------
+ |   Option       | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) -> (##Type_ ℓ[32m[1][0m)
+
+(##_≡>_ (_:_ ℓ TypeLevel) (##_->_ (_:_ a (##Type_ ℓ)) (##Type_ ℓ)))
+
+ |   some         | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (a[32m[0][0m -> (Option[32m[103][0m ℓ[32m[2][0m a[32m[1][0m))
+
+(##_->_ ?a (Option ?a))
+
+ |   none         | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (Option[32m[102][0m ℓ[32m[1][0m a[32m[0][0m)
+
+(##_≡>_ (_:_ ℓ TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (Option a)))
+
+ |   optionally   | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[1][0m)) ≡> (b : (##Type_ ℓ[32m[1][0m)) ≡> ((a[32m[1][0m -> b[32m[1][0m) -> (b[32m[1][0m -> ((Option[32m[106][0m ℓ[32m[5][0m a[32m[3][0m) -> b[32m[3][0m)))
+
+(##_->_ (##_->_ ?a ?b) (##_->_ ?b (##_->_ (Option ?a) ?b)))
+
+ |   List_leng…   | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> ((List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m) -> Int[32m[255][0m)
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (List a) Int)))
+
+ |   List_head1   | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (xs : (List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m)) -> (Option[32m[103][0m ℓ[32m[2][0m a[32m[1][0m)
+
+(##_≡>_ (_:_ ℓ TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (_:_ xs (List a)) (Option a))))
+
+ |   List_head    | 
+(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ[32m[0][0m)) ≡> (x : τ[32m[0][0m) -> (xs : (List[32m[158][0m ℓ[32m[2][0m τ[32m[1][0m)) -> τ[32m[2][0m
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ τ (##Type_ ℓ)) (##_->_ (_:_ x τ) (##_->_ (_:_ xs (List τ)) τ))))
+
+ |   List_tail    | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (xs : (List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m)) -> (List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m)
+
+(##_->_ (_:_ xs (List ?a)) (List ?a))
+
+ |   List_map     | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[1][0m)) ≡> (b : (##Type_ ℓ[32m[1][0m)) ≡> ((a[32m[1][0m -> b[32m[1][0m) -> ((List[32m[160][0m ℓ[32m[4][0m a[32m[2][0m) -> (List[32m[161][0m ℓ[32m[4][0m b[32m[2][0m)))
+
+(##_->_ (##_->_ ?a ?b) (##_->_ (List ?a) (List ?b)))
+
+ |   List_foldr   | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (b : (##Type_ ℓ[32m[1][0m)) ≡> (a : (##Type_ ℓ[32m[1][0m)) ≡> ((b[32m[1][0m -> (a[32m[1][0m -> a[32m[2][0m)) -> ((List[32m[160][0m ℓ[32m[4][0m b[32m[2][0m) -> (a[32m[2][0m -> a[32m[3][0m)))
+
+(##_->_ (##_->_ ?b (##_->_ ?a ?a)) (##_->_ (List ?b) (##_->_ ?a ?a)))
+
+ |   List_find    | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> ((a[32m[0][0m -> Bool[32m[211][0m) -> ((List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m) -> (Option[32m[104][0m ℓ[32m[3][0m a[32m[2][0m)))
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (##_->_ a Bool) (##_->_ (List a) (Option a)))))
+
+ |   List_nth     | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (Int[32m[254][0m -> ((List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m) -> (a[32m[2][0m -> a[32m[3][0m)))
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ Int (##_->_ (List a) (##_->_ a a)))))
+
+ |   Sexp_error   | 
+Sexp[32m[249][0m
+
+Sexp
+
+ |   Sexp_to_l…   | 
+(s : ##Sexp) -> (exceptions : (List[32m[156][0m ##TypeLevel.z ##Sexp)) -> (List[32m[157][0m ##TypeLevel.z ##Sexp)
+
+(##_->_ (_:_ s ##Sexp) (##_->_ (_:_ exceptions (List ##Sexp)) (List ##Sexp)))
+
+ |   multiarg_…   | 
+(name : ##String) -> (margs : (List[32m[156][0m ##TypeLevel.z Sexp[32m[250][0m)) -> (IO[32m[255][0m ##Sexp)
+
+(##_->_ (_:_ name ##String) (##_->_ (_:_ margs (List Sexp)) (IO ##Sexp)))
+
+ |   lambda_->_   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   lambda_=>_   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   lambda_…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   List_reve…   | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> ((List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m) -> ((List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m) -> (List[32m[159][0m ℓ[32m[3][0m a[32m[2][0m)))
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (List a) (##_->_ (List a) (List a)))))
+
+ |   List_conc…   | 
+(ℓ : TypeLevel[32m[242][0m) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (l : (List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m)) -> (t : (List[32m[158][0m ℓ[32m[2][0m a[32m[1][0m)) -> (List[32m[159][0m ℓ[32m[3][0m a[32m[2][0m)
+
+(##_≡>_ (_:_ ℓ TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (_:_ l (List a)) (##_->_ (_:_ t (List a)) (List a)))))
+
+ |   List_foldl   | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[1][0m)) ≡> (b : (##Type_ ℓ[32m[1][0m)) ≡> ((a[32m[1][0m -> (b[32m[1][0m -> a[32m[3][0m)) -> (a[32m[2][0m -> ((List[32m[161][0m ℓ[32m[4][0m b[32m[2][0m) -> a[32m[4][0m)))
+
+(##_->_ (##_->_ ?a (##_->_ ?b ?a)) (##_->_ ?a (##_->_ (List ?b) ?a)))
+
+ |   List_mapi    | 
+(a : Type[32m[245][0m) ≡> (b : Type[32m[246][0m) ≡> ((a[32m[1][0m -> (Int[32m[255][0m -> b[32m[2][0m)) -> ((List[32m[158][0m ##TypeLevel.z a[32m[2][0m) -> (List[32m[159][0m ##TypeLevel.z b[32m[2][0m)))
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (##_->_ a (##_->_ Int b)) (##_->_ (List a) (List b)))))
+
+ |   List_map2    | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[2][0m)) ≡> (b : (##Type_ ℓ[32m[2][0m)) ≡> (c : (##Type_ ℓ[32m[2][0m)) ≡> ((a[32m[2][0m -> (b[32m[2][0m -> c[32m[2][0m)) -> ((List[32m[162][0m ℓ[32m[6][0m a[32m[3][0m) -> ((List[32m[163][0m ℓ[32m[6][0m b[32m[3][0m) -> (List[32m[164][0m ℓ[32m[6][0m c[32m[3][0m))))
+
+(##_->_ (##_->_ ?a (##_->_ ?b ?c)) (##_->_ (List ?a) (##_->_ (List ?b) (List ?c))))
+
+ |   List_fold2   | 
+(ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[2][0m)) ≡> (b : (##Type_ ℓ[32m[2][0m)) ≡> (c : (##Type_ ℓ[32m[2][0m)) ≡> ((a[32m[2][0m -> (b[32m[2][0m -> (c[32m[2][0m -> a[32m[5][0m))) -> (a[32m[3][0m -> ((List[32m[163][0m ℓ[32m[6][0m b[32m[3][0m) -> ((List[32m[164][0m ℓ[32m[6][0m c[32m[3][0m) -> a[32m[6][0m))))
+
+(##_->_ (##_->_ ?a (##_->_ ?b (##_->_ ?c ?a))) (##_->_ ?a (##_->_ (List ?b) (##_->_ (List ?c) ?a))))
+
+ |   List_empty   | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> ((List[32m[157][0m ℓ[32m[1][0m a[32m[0][0m) -> Bool[32m[211][0m)
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ (List a) Bool)))
+
+ |   I            | 
+(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ[32m[0][0m)) ≡> (x : τ[32m[0][0m) -> τ[32m[1][0m
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ τ (##Type_ ℓ)) (##_->_ (_:_ x τ) τ)))
+
+ |   K            | 
+(ℓ : ##TypeLevel) ≡> (a : (##Type_ ℓ[32m[0][0m)) ≡> (a[32m[0][0m -> (b : Type[32m[248][0m) ≡> (b[32m[0][0m -> a[32m[3][0m))
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_≡>_ (_:_ a (##Type_ ℓ)) (##_->_ a (##_≡>_ (_:_ b Type) (##_->_ b a)))))
+
+ |   quote1       | 
+(Sexp[32m[249][0m -> Sexp[32m[250][0m)
+
+(##_->_ Sexp Sexp)
+
+ |   quote        | 
+Macro[32m[146][0m
+
+Macro
+
+ |   make-decl    | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> Sexp[32m[251][0m))
+
+(##_->_ Sexp (##_->_ Sexp Sexp))
+
+ |   chain-decl   | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> Sexp[32m[251][0m))
+
+(##_->_ Sexp (##_->_ Sexp Sexp))
+
+ |   chain-dec…   | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> (Sexp[32m[251][0m -> Sexp[32m[252][0m)))
+
+(##_->_ Sexp (##_->_ Sexp (##_->_ Sexp Sexp)))
+
+ |   make-cons    | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> Sexp[32m[251][0m))
+
+(##_->_ Sexp (##_->_ Sexp Sexp))
+
+ |   make-ann     | 
+(Sexp[32m[249][0m -> (Sexp[32m[250][0m -> Sexp[32m[251][0m))
+
+(##_->_ Sexp (##_->_ Sexp Sexp))
+
+ |   type-impl    | 
+(x : (List[32m[155][0m ##TypeLevel.z Sexp[32m[249][0m)) -> (IO[32m[254][0m ##Sexp)
+
+(##_->_ (_:_ x (List Sexp)) (IO ##Sexp))
+
+ |   type_        | 
+Macro[32m[146][0m
+
+Macro
+
+ |   Sexp_wrap…   | 
+Type[32m[245][0m
+
+Type
+
+ |   node         | 
+(Sexp[32m[249][0m -> ((List[32m[156][0m ##TypeLevel.z Sexp[32m[250][0m) -> Sexp_wrapper[32m[66][0m))
+
+(##_->_ Sexp (##_->_ (List Sexp) Sexp_wrapper))
+
+ |   symbol       | 
+(String[32m[246][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ String Sexp_wrapper)
+
+ |   string       | 
+(String[32m[246][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ String Sexp_wrapper)
+
+ |   integer      | 
+(Integer[32m[251][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ Integer Sexp_wrapper)
+
+ |   float        | 
+(Float[32m[254][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ Float Sexp_wrapper)
+
+ |   block        | 
+(Sexp[32m[249][0m -> Sexp_wrapper[32m[65][0m)
+
+(##_->_ Sexp Sexp_wrapper)
+
+ |   Sexp_wrap    | 
+(s : ##Sexp) -> [35mtypecons[0m (Sexp_wrapper)   (block Sexp[32m[250][0m) (float Float[32m[255][0m) (integer Integer[32m[252][0m) (node Sexp[32m[250][0m (List[32m[157][0m ##TypeLevel.z Sexp[32m[251][0m)) (string String[32m[247][0m) (symbol String[32m[247][0m)
+
+(##_->_ (_:_ s ##Sexp) (##typecons (Sexp_wrapper) (block Sexp) (float Float) (integer Integer) (node Sexp (List Sexp)) (string String) (symbol String)))
+
+ |   BoolMod      | 
+([35mlambda [0m(t1 : (##Type_ (##TypeLevel.succ ##TypeLevel.z))) -> [35mlambda [0m(t2 : (##Type_ ##TypeLevel.z)) -> [35mlambda [0m(t3 : (##Type_ ##TypeLevel.z)) -> [35mtypecons[0m (_)   (cons t1[32m[2][0m t2[32m[2][0m t3[32m[2][0m) (##Type_ ##TypeLevel.z) [35mtypecons[0m (Bool)   (false) (true) [35mtypecons[0m (Bool)   (false) (true))
+
+((##lambda_->_ (_:_ t1 (##Type_ (##TypeLevel.succ ##TypeLevel_z))) (##lambda_->_ (_:_ t2 (##Type_ ##TypeLevel_z)) (##lambda_->_ (_:_ t3 (##Type_ ##TypeLevel_z)) (##typecons (_) (cons (_::_ t t1) (_::_ true t2) (_::_ false t3)))))) (##Type_ ##TypeLevel_z) (typecons Bool true false) (typecons Bool true false))
+
+ |   Pair         | 
+(a : Type[32m[245][0m) -> (b : Type[32m[246][0m) -> (##Type_ ##TypeLevel.z)
+
+(##_->_ (_:_ a Type) (##_->_ (_:_ b Type) (##Type_ ##TypeLevel_z)))
+
+ |   pair         | 
+(a : Type[32m[245][0m) ≡> (b : Type[32m[246][0m) ≡> (fst : a[32m[1][0m) -> (snd : b[32m[1][0m) -> (Pair[32m[59][0m a[32m[3][0m b[32m[2][0m)
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_->_ (_:_ fst a) (##_->_ (_:_ snd b) (Pair a b)))))
+
+ |   Triplet      | 
+(a : Type[32m[245][0m) -> (b : Type[32m[246][0m) -> (c : Type[32m[247][0m) -> Type[32m[248][0m
+
+(##_->_ (_:_ a Type) (##_->_ (_:_ b Type) (##_->_ (_:_ c Type) Type)))
+
+ |   triplet      | 
+(a : Type[32m[245][0m) ≡> (b : Type[32m[246][0m) ≡> (c : Type[32m[247][0m) ≡> (x : a[32m[2][0m) -> (y : b[32m[2][0m) -> (z : c[32m[2][0m) -> (Triplet[32m[59][0m a[32m[5][0m b[32m[4][0m c[32m[3][0m)
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ b Type) (##_≡>_ (_:_ c Type) (##_->_ (_:_ x a) (##_->_ (_:_ y b) (##_->_ (_:_ z c) (Triplet a b c)))))))
+
+ |   List_merge   | 
+(a : (##Type_ ##TypeLevel.z)) ≡> (b : (##Type_ ##TypeLevel.z)) ≡> ((List[32m[157][0m ##TypeLevel.z a[32m[1][0m) -> ((List[32m[158][0m ##TypeLevel.z b[32m[1][0m) -> (List[32m[159][0m ##TypeLevel.z (Pair[32m[59][0m a[32m[3][0m b[32m[2][0m))))
+
+(##_->_ (List ?a) (##_->_ (List ?b) (List (Pair ?a ?b))))
+
+ |   List_map-…   | 
+(τ : (##Type_ ##TypeLevel.z)) ≡> (b : Type[32m[246][0m) ≡> (xs : (List[32m[157][0m ##TypeLevel.z (Pair[32m[57][0m τ[32m[1][0m b[32m[0][0m))) -> (List[32m[158][0m ##TypeLevel.z τ[32m[2][0m)
+
+(##_->_ (_:_ xs (List (Pair ?τ ?b))) (List ?τ))
+
+ |   List_map-…   | 
+(a : Type[32m[245][0m) ≡> (τ : (##Type_ ##TypeLevel.z)) ≡> (xs : (List[32m[157][0m ##TypeLevel.z (Pair[32m[57][0m a[32m[1][0m τ[32m[0][0m))) -> (List[32m[158][0m ##TypeLevel.z τ[32m[1][0m)
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ τ (##Type_ ##TypeLevel_z)) (##_->_ (_:_ xs (List (Pair a τ))) (List τ))))
+
+ |   False        | 
+(##Type_ ##TypeLevel.z)
+
+(##Type_ ##TypeLevel_z)
+
+ |   True         | 
+(##Type_ ##TypeLevel.z)
+
+(##Type_ ##TypeLevel_z)
+
+ |   Not          | 
+(ℓ : ##TypeLevel) ≡> (prop : (##Type_ ℓ[32m[0][0m)) -> (##Type_ ℓ[32m[1][0m)
+
+(##_≡>_ (_:_ ℓ ##TypeLevel) (##_->_ (_:_ prop (##Type_ ℓ)) (##Type_ ℓ)))
+
+ |   Decidable    | 
+(ℓ : ##TypeLevel) => (prop : (##Type_ ℓ[32m[0][0m)) -> (##Type_ ℓ[32m[1][0m)
+
+(##_=>_ (_:_ ℓ ##TypeLevel) (##_->_ (_:_ prop (##Type_ ℓ)) (##Type_ ℓ)))
+
+ |   LList        | 
+(Type[32m[245][0m -> (Int[32m[253][0m -> Type[32m[247][0m))
+
+(##_->_ Type (##_->_ Int Type))
+
+ |   vnil         | 
+(a : Type[32m[245][0m) ≡> (n : Int[32m[253][0m) ≡> (p : (Eq[32m[259][0m ##TypeLevel.z ##Int n[32m[0][0m (Integer->Int[32m[185][0m [33m0[0m))) ≡> (LList[32m[47][0m a[32m[2][0m n[32m[1][0m)
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ n Int) (##_≡>_ (_:_ p (Eq n (Integer->Int (##typer-immediate 0)))) (LList a n))))
+
+ |   vcons        | 
+(a : Type[32m[245][0m) ≡> (n : Int[32m[253][0m) ≡> (n1 : Int[32m[254][0m) ≡> (a[32m[2][0m -> ((LList[32m[48][0m a[32m[3][0m n1[32m[1][0m) -> (p : (Eq[32m[262][0m ##TypeLevel.z ##Int n[32m[3][0m (Int_+[32m[210][0m n1[32m[2][0m (Integer->Int[32m[188][0m [33m1[0m)))) ≡> (LList[32m[50][0m a[32m[5][0m n[32m[4][0m)))
+
+(##_≡>_ (_:_ a Type) (##_≡>_ (_:_ n Int) (##_≡>_ (_:_ n1 Int) (##_->_ a (##_->_ (LList a n1) (##_≡>_ (_:_ p (Eq n (Int_+ n1 (Integer->Int (##typer-immediate 1))))) (LList a n)))))))
+
+ |   if_then_e…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   not          | 
+(Bool[32m[208][0m -> Bool[32m[209][0m)
+
+(##_->_ Bool Bool)
+
+ |   or           | 
+(Bool[32m[208][0m -> (Bool[32m[209][0m -> Bool[32m[210][0m))
+
+(##_->_ Bool (##_->_ Bool Bool))
+
+ |   and          | 
+(Bool[32m[208][0m -> (Bool[32m[209][0m -> Bool[32m[210][0m))
+
+(##_->_ Bool (##_->_ Bool Bool))
+
+ |   xor          | 
+(Bool[32m[208][0m -> (Bool[32m[209][0m -> Bool[32m[210][0m))
+
+(##_->_ Bool (##_->_ Bool Bool))
+
+ |   fold         | 
+(Bool[32m[208][0m -> (a : Type[32m[246][0m) ≡> (a[32m[0][0m -> (a[32m[1][0m -> a[32m[2][0m)))
+
+(##_->_ Bool (##_≡>_ (_:_ a Type) (##_->_ a (##_->_ a a))))
+
+ |   test1        | 
+(Option[32m[100][0m ##TypeLevel.z Int[32m[252][0m)
+
+(Option Int)
+
+ |   test2        | 
+(Option[32m[100][0m ##TypeLevel.z Int[32m[252][0m)
+
+(Option Int)
+
+ |   test3        | 
+(Option[32m[100][0m ##TypeLevel.z Int[32m[252][0m)
+
+(Option Int)
+
+ |   test4        | 
+(Option[32m[100][0m ##TypeLevel.z Int[32m[252][0m)
+
+(Option Int)
+
+ |   Elab_nth-…   | 
+(a : ##String) -> (b : ##Int) -> (c : ##Elab_Context) -> (Option[32m[103][0m ##TypeLevel.z ##String)
+
+(##_->_ (_:_ a ##String) (##_->_ (_:_ b ##Int) (##_->_ (_:_ c ##Elab_Context) (Option ##String))))
+
+ |   Elab_arg-…   | 
+(a : ##String) -> (b : ##String) -> (c : ##Elab_Context) -> (Option[32m[103][0m ##TypeLevel.z ##Int)
+
+(##_->_ (_:_ a ##String) (##_->_ (_:_ b ##String) (##_->_ (_:_ c ##Elab_Context) (Option ##Int))))
+
+ |   poly-lits    | 
+[35mtypecons[0m (record)   (cons (α : Type[32m[245][0m) -> Type[32m[246][0m (α : Type[32m[246][0m) ≡> (fromInteger : (Integer[32m[253][0m -> α[32m[1][0m)) -> ([35mlet [0mFromInteger : (α : Type[32m[248][0m) -> Type[32m[249][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[249][0m))  (mkFromInteger (Integer[32m[256][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[249][0m))  (mkFromInteger (Integer[32m[256][0m -> α[32m[1][0m)) α[32m[1][0m) (α : Type[32m[247][0m) ≡> (inst : ([35mlet [0mFromInteger : (α : Type[32m[248][0m) -> Type[32m[249][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[249][0m))  (mkFromInteger (Integer[32m[256][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[249][0m))  (mkFromInteger (Integer[32m[256][0m -> α[32m[1][0m)) α[32m[0][0m)) => (Integer[32m[255][0m -> α[32m[2][0m) Macro[32m[149][0m ([35mlet [0mFromInteger : (α : Type[32m[249][0m) -> Type[32m[250][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[250][0m))  (mkFromInteger (Integer[32m[257][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[250][0m))  (mkFromInteger (Integer[32m[257][0m -> α[32m[1][0m)) Integer[32m[255][0m) ([35mlet [0mFromInteger : (α : Type[32m[250][0m) -> Type[32m[251][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[251][0m))  (mkFromInteger (Integer[32m[258][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[251][0m))  (mkFromInteger (Integer[32m[258][0m -> α[32m[1][0m)) Int[32m[257][0m))
+
+(##typecons (record) (cons (_::_ FromInteger (_->_ (_:_ α Type) Type)) (_::_ mkFromInteger (##_≡>_ (_:_ α Type) (##_->_ (_:_ fromInteger (##_->_ Integer α)) ((##let_in_ (_;_ (_:_ FromInteger (_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) α)))) (_::_ fromInteger (##_≡>_ (_:_ α Type) (##_=>_ (_:_ inst ((##let_in_ (_;_ (_:_ FromInteger (_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) α)) (##_->_ Integer α)))) (_::_ typer-immediate Macro) (_::_ IntegerFromInteger ((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) Integer)) (_::_ IntFromInteger ((##let_in_ (_;_ (_:_ FromInteger (_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) Int))))
+
+ |   typer-imm…   | 
+Macro[32m[146][0m
+
+Macro
+
+ |   FromInteg…   | 
+(α : Type[32m[245][0m) -> Type[32m[246][0m
+
+(_->_ (_:_ α Type) Type)
+
+ |   mkFromInt…   | 
+(α : Type[32m[245][0m) ≡> (fromInteger : (Integer[32m[252][0m -> α[32m[1][0m)) -> ([35mlet [0mFromInteger : (α : Type[32m[247][0m) -> Type[32m[248][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[248][0m))  (mkFromInteger (Integer[32m[255][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[248][0m))  (mkFromInteger (Integer[32m[255][0m -> α[32m[1][0m)) α[32m[1][0m)
+
+(##_≡>_ (_:_ α Type) (##_->_ (_:_ fromInteger (##_->_ Integer α)) ((##let_in_ (_;_ (_:_ FromInteger (_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) α)))
+
+ |   fromInteg…   | 
+(α : Type[32m[245][0m) ≡> (inst : ([35mlet [0mFromInteger : (α : Type[32m[246][0m) -> Type[32m[247][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[247][0m))  (mkFromInteger (Integer[32m[254][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[247][0m))  (mkFromInteger (Integer[32m[254][0m -> α[32m[1][0m)) α[32m[0][0m)) => (Integer[32m[253][0m -> α[32m[2][0m)
+
+(##_≡>_ (_:_ α Type) (##_=>_ (_:_ inst ((##let_in_ (_;_ (_:_ FromInteger (_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) α)) (##_->_ Integer α)))
+
+ |   IntFromIn…   | 
+([35mlet [0mFromInteger : (α : Type[32m[245][0m) -> Type[32m[246][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[246][0m))  (mkFromInteger (Integer[32m[253][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[246][0m))  (mkFromInteger (Integer[32m[253][0m -> α[32m[1][0m)) Int[32m[252][0m)
+
+((##let_in_ (_;_ (_:_ FromInteger (##_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) Int)
+
+ |   IntegerFr…   | 
+([35mlet [0mFromInteger : (α : Type[32m[245][0m) -> Type[32m[246][0m; FromInteger = [35mtypecons[0m (FromInteger (α : Type[32m[246][0m))  (mkFromInteger (Integer[32m[253][0m -> α[32m[1][0m))[35m in [0m [35mtypecons[0m (FromInteger (α : Type[32m[246][0m))  (mkFromInteger (Integer[32m[253][0m -> α[32m[1][0m)) Integer[32m[251][0m)
+
+((##let_in_ (_;_ (_:_ FromInteger (_->_ (_:_ α Type) Type)) (_=_ FromInteger (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (_->_ Integer α)))))) (##typecons (FromInteger (_:_ α Type)) (mkFromInteger (_:_ fromInteger (##_->_ Integer α))))) Integer)
+
+ |   monads       | 
+[35mtypecons[0m (record)   (cons (M : (Type[32m[245][0m -> Type[32m[246][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)) (M : (Type[32m[246][0m -> Type[32m[247][0m)) ≡> (bind : (a : Type[32m[247][0m) ≡> (b : Type[32m[248][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m)))) -> (pure : (a : Type[32m[248][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) -> ([35mlet [0mMonad : (M : (Type[32m[249][0m -> Type[32m[250][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) M[32m[2][0m) (M : (Type[32m[247][0m -> Type[32m[248][0m)) ≡> (monad : ([35mlet [0mMonad : (M : (Type[32m[248][0m -> Type[32m[249][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[249][0m -> Type[32m[250][0m)))  (mkMonad (a : Type[32m[250][0m) ≡> (b : Type[32m[251][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[251][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[249][0m -> Type[32m[250][0m)))  (mkMonad (a : Type[32m[250][0m) ≡> (b : Type[32m[251][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[251][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) M[32m[0][0m)) => (a : Type[32m[249][0m) ≡> (b : Type[32m[250][0m) ≡> ((M[32m[3][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[5][0m b[32m[2][0m)) -> (M[32m[5][0m b[32m[2][0m))) (M : (Type[32m[248][0m -> Type[32m[249][0m)) ≡> (monad : ([35mlet [0mMonad : (M : (Type[32m[249][0m -> Type[32m[250][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) M[32m[0][0m)) => (a : Type[32m[250][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)) ([35mlet [0mMonad : (M : (Type[32m[249][0m -> Type[32m[250][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[250][0m -> Type[32m[251][0m)))  (mkMonad (a : Type[32m[251][0m) ≡> (b : Type[32m[252][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[252][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) IO[32m[257][0m) (a : Type[32m[250][0m) ≡> (b : Type[32m[251][0m) ≡> ((Option[32m[107][0m ##TypeLevel.z a[32m[1][0m) -> ((a[32m[2][0m -> (Option[32m[109][0m ##TypeLevel.z b[32m[2][0m)) -> (Option[32m[109][0m ##TypeLevel.z b[32m[2][0m))) (a : Type[32m[251][0m) ≡> (a[32m[0][0m -> (Option[32m[108][0m ##TypeLevel.z a[32m[1][0m)) ([35mlet [0mMonad : (M : (Type[32m[252][0m -> Type[32m[253][0m)) -> (##Type_ (##TypeLevel.succ ##TypeLevel.z)); Monad = [35mtypecons[0m (Monad (M : (Type[32m[253][0m -> Type[32m[254][0m)))  (mkMonad (a : Type[32m[254][0m) ≡> (b : Type[32m[255][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[255][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m)))[35m in [0m [35mtypecons[0m (Monad (M : (Type[32m[253][0m -> Type[32m[254][0m)))  (mkMonad (a : Type[32m[254][0m) ≡> (b : Type[32m[255][0m) ≡> ((M[32m[2][0m a[32m[1][0m) -> ((a[32m[2][0m -> (M[32m[4][0m b[32m[2][0m)) -> (M[32m[4][0m b[32m[2][0m))) (a : Type[32m[255][0m) ≡> (a[32m[0][0m -> (M[32m[3][0m a[32m[1][0m))) (Option[32m[107][0m ##TypeLevel.z)))
=====================================
src/REPL.ml
=====================================
@@ -213,6 +213,12 @@ let rec repl i (interactive : #Backend.interactive) (ectx : elab_context) =
                 | _       -> Heuristic.print_heur_ctx (ectx) in
               ectx
+          | "%tctx"::args | "%tc"::args
+            -> let _ = match args with
+                | ["all"] -> Heuristic.test_dump_heur_ctx (ectx)
+                | _       -> Heuristic.test_print_heur_ctx (ectx) in
+              ectx
+
| cmd::_
             -> error {|"%s" is not a correct REPL command|} cmd;
=====================================
src/debruijn.ml
=====================================
@@ -465,16 +465,20 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem  =
       | (((_, Some name), _, _), Some ename)
         -> (* Check if names match *)
            if not (ename = name) then
-             let print_action =
+             let _print_action =
                if !log_full_lctx
                then fun () -> (print_lexp_ctx ctx; print_newline ())
                else fun () -> summarize_lctx ctx dbi
              in
+
+             ignore dsinfo
+             (*
              fatal
                ~loc:(sexp_location loc) ~print_action
                ({|DeBruijn index %d refers to wrong name.  |}
                 ^^ {|Expected: "%s" got "%s"|})
                dbi ename name
+              *)
       | _ -> () in
ret
=====================================
src/elab.ml
=====================================
@@ -170,7 +170,7 @@ let elab_check_proper_type (ctx : elab_context) ltp var =
                     | (_, None) -> ""
                     | (_, Some name) -> " of var `" ^ name ^ "`");
                  raise e
-
+(*
 let elab_check_def (ctx : elab_context) var lxp ltype =
   let lctx = ectx_to_lctx ctx in
   let loc = lexp_sinfo lxp in
@@ -211,13 +211,14 @@ let elab_check_def (ctx : elab_context) var lxp ltype =
       ])
       ~loc:(sexp_location loc)
       "Type check error: ¡¡ctx_define error!!"
+*)
let ctx_extend (ctx: elab_context) (var : vname) def ltype =
   elab_check_proper_type ctx ltype var;
   ectx_extend ctx var def ltype
let ctx_define (ctx: elab_context) var lxp ltype =
-  elab_check_def ctx var lxp ltype;
+  (*elab_check_def ctx var lxp ltype;*)
   ectx_extend ctx var (LetDef (0, lxp)) ltype
let ctx_define_rec (ctx: elab_context) decls =
@@ -228,12 +229,13 @@ let ctx_define_rec (ctx: elab_context) decls =
                             n - 1)
                          (List.length decls)
                          decls in
-  let _ = List.fold_left (fun n (var, lxp, ltp)
+
+(*  let _ = List.fold_left (fun n (var, lxp, ltp)
                           -> elab_check_def nctx var lxp
                                            (push_susp ltp (S.shift n));
                             n - 1)
                          (List.length decls)
-                         decls in
+                         decls in *)
   nctx
(*  The main job of lexp (currently) is to determine variable name (index)
@@ -599,8 +601,10 @@ let wrapLambda ne vname t _l e =
 let elab_p_id ((l,name) : symbol) : vname =
   (Symbol (l, name), match name with "_" -> None | _ -> Some name)
+let hc_elab_table = OL.LMap.create 1000
+
 (* Infer or check, as the case may be.  *)
-let rec elaborate ctx se ot =
+let rec elaborate' ctx se ot =
   let (e, res_t) = match se with
   (* Rewrite SYM to `typer-identifier SYM`.  *)
   | Symbol ((loc, name) as _id)
@@ -642,6 +646,11 @@ let rec elaborate ctx se ot =
              (check_inferred ctx e inferred_t t, Checked))
   | _ -> (e, res_t)
+and elaborate ctx se ot =
+  let (le, res_t) = elaborate' ctx se ot in
+  OL.LMap.add hc_elab_table le se;
+  (le,res_t)
+
 and infer (p : sexp) (ctx : elab_context): lexp * ltype =
   match elaborate ctx p None with
   | (_, Checked) -> fatal ~loc:(sexp_location p) "`infer` got Checked!"
@@ -811,7 +820,9 @@ and check_case rtype (loc, target, ppatterns) ctx =
     let tknd = OL.get_type (ectx_to_lctx ctx) tltp in
     let tlvl = match OL.lexp'_whnf tknd (ectx_to_lctx ctx) with
       | Sort (_, Stype l) -> l
-      | _ -> fatal "Target lexp's kind is not a sort" in
+      | _ -> (error ~loc:(lexp_location tlxp) "Target lexp's kind is not a sort";
+            tltp)
+    in
     let it_cs_as = ref None in
     let ltarget = ref tlxp in
@@ -1428,7 +1439,7 @@ and lexp_decls_1
   in (EV.set_getenv nctx;
       let res = lexp_decls_1 sdecls tokens nctx
                   pending_decls pending_defs in
-        (Log.stop_on_error (); res))
+        ((*Log.stop_on_error ();*) res))
(* Why is the return value a list of list?
    - each `(vname * lexp * ltype)` is a definition
@@ -1444,18 +1455,18 @@ and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context)
     | _ ->
        let decls, sdecls, tokens, nctx =
          lexp_decls_1 sdecls tokens ctx ctx SMap.empty [] in
-       Log.stop_on_error ();
+       (* Log.stop_on_error (); *)
        let declss, nnctx = impl sdecls tokens nctx in
        decls :: declss, nnctx in
   impl sdecls tokens ctx
and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list =
   let res = List.map (fun pe -> let e, _ = infer pe ctx in e) p in
-    (Log.stop_on_error (); res)
+    ((* Log.stop_on_error (); *) res)
and lexp_parse_sexp (ctx: elab_context) (s : sexp) : lexp =
   let e, _ = infer s ctx in
-  (Log.stop_on_error (); e)
+  ((* Log.stop_on_error (); *) e)
(* --------------------------------------------------------------------------
  *  Special forms implementation
=====================================
src/heuristic.ml
=====================================
@@ -15,13 +15,18 @@ let mkMetavar_1 name =
   let meta = Unif.create_metavar_1 (-437) impossible (-1) in
   mkMetavar (meta, S.identity, name)
-(* ugly printing (sexp_pri
-nt (pexp_unparse (heuristic_unparse e))) *)
+let mkMetavar_2 =
+  let meta = Unif.create_metavar_1 (-437) impossible (-1) in
+  mkMetavar (meta, S.identity, (DB.dsinfo, Some ""))
+
+(* ugly printing (sexp_print (pexp_unparse (heuristic_unparse e))) *)
 let heuristic_unparse cf lxp =
   let rec loop lxp =
-    if cf 2 == 42 then lexp_sinfo lxp
-    else
-      match lexp_lexp' lxp with
+    match cf == 42 with
+    | true -> lexp_sinfo lxp
+    | _ -> match OL.LMap.find_opt Elab.hc_elab_table lxp with
+      | Some s -> s
+      | _ -> match lexp_lexp' lxp with
         | Susp _
           -> loop (nosusp lxp)
         | Imm (sexp)
@@ -30,7 +35,7 @@ let heuristic_unparse cf lxp =
           -> Symbol (l, "##" ^ name)
         | Var ((loc, name), _)
           -> Symbol (sexp_location loc, maybename name)
-        | Proj (l,lxp,(loc,str))
+        | Proj (l, lxp, (loc,str))
           -> Node (Symbol (sexp_location l, "__.__"),
                    [(loop lxp);(Symbol (loc,str))])
         | Cons (t, (l, name))
@@ -40,48 +45,59 @@ let heuristic_unparse cf lxp =
         | Lambda (kind, vdef, ltp, body)
           -> let l = lexp_location lxp in
             let st = loop ltp in
-            if kind != Anormal && cf 2 == 0
-            then loop body
-            else Node (Symbol (l, match kind with
-                                  | Anormal -> "##lambda_->_"
-                                  | Aimplicit -> "##lambda_=>_"
-                                  | Aerasable -> "##lambda_≡>_"),
-                       [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]);
-                        loop body])
+            (match cf == 2 && kind != Anormal with
+              | true -> loop body
+              | _ -> Node (Symbol (l, match kind with
+                                       | Anormal -> "##lambda_->_"
+                                       | Aimplicit -> "##lambda_=>_"
+                                       | Aerasable -> "##lambda_≡>_"),
+                            [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]);
+                             loop body])
+            )
| Arrow (loc, arg_kind, (l, oname), ltp1, ltp2)
           -> let ut1 = loop ltp1 in
-             if arg_kind != Anormal && cf 2 == 0
-             then loop (mkSusp ltp2 (S.substitute (mkMetavar_1  (l, oname))))
-             else Node (Symbol (sexp_location loc, match arg_kind with
-                                                  | Anormal -> "_->_"
-                                                  | Aimplicit -> "_=>_"
-                                                  | Aerasable -> "_≡>_"),
-                   [(match oname with None -> ut1
-                                    | Some v -> Node (Symbol (sexp_location l, "_:_"),
-                                                     [Symbol (sexp_location l,v); ut1]));
-                    loop ltp2])
+             (match cf == 2 && arg_kind != Anormal with
+                | true -> loop (mkSusp ltp2 (S.substitute (mkMetavar_1  (l, oname))))
+                | _ -> Node (Symbol (sexp_location loc, match arg_kind with
+                                                         | Anormal -> "##_->_"
+                                                         | Aimplicit -> "##_=>_"
+                                                         | Aerasable -> "##_≡>_"),
+                            [(match oname with None -> ut1
+                                             | Some v -> Node (Symbol (sexp_location l, "_:_"),
+                                                              [Symbol (sexp_location l,v); ut1]));
+                             loop ltp2])
+             )
| Let (loc, ldecls, body)
           -> (* (vdef * lexp * ltype) list *)
            let sdecls = List.fold_left
-                          (fun acc (vdef, lxp, ltp)
-                           -> Node (Symbol (lexp_location lxp, "_=_"),
-                                   [Symbol (sname vdef); loop ltp])
-                             :: Node (Symbol (lexp_location lxp, "_=_"),
-                                      [Symbol (sname vdef); loop lxp])
-                             :: acc)
-                          [] ldecls in
+                          (match cf == 2 with
+                             | true -> (fun acc (vdef, lxp, ltp)
+                                        -> Node (Symbol (U.dummy_location, "_:_"),
+                                                [Symbol (sname vdef); lexp_unparse ltp])
+                                          :: Node (Symbol (U.dummy_location, "_=_"),
+                                                   [Symbol (sname vdef); lexp_unparse lxp])
+                                          :: acc)
+                             | _ -> (fun acc (vdef, lxp, ltp)
+                                     -> Node (Symbol (lexp_location lxp, "_:_"),
+                                             [Symbol (sname vdef); if cf == 1 then loop ltp else loop (mkSusp ltp  (S.substitute mkMetavar_2))])
+                                       :: Node (Symbol (lexp_location lxp, "_=_"),
+                                                [Symbol (sname vdef); loop lxp])
+                                       :: acc)
+                          ) [] ldecls in
            Node (Symbol (sexp_location loc, "##let_in_"),
                  [Node (Symbol (sexp_location loc, "_;_"), sdecls);
                   loop body])
| Call (_, lxp, largs)
           -> (* (arg_kind * lexp) list *)
-          let fargs = List.filter ( fun (kind, _) -> if cf 2 == 0 then kind = Anormal else kind != Anormal ) largs in
-            let sargs = List.map ( fun (_, elem) -> loop elem) fargs in
+          (* let fargs = List.filter ( fun (kind, _) -> if cf 2 == 0 then kind = Anormal else kind != Anormal ) largs in *)
+          let fargs = List.filter ( fun (kind, _) -> kind = Anormal ) largs in
+            let sargs = List.map ( fun (_, elem) -> loop elem ) fargs in
               Node (loop lxp, sargs)
+
         | Inductive (loc, label, lfargs, ctors)
           -> (* (arg_kind * vdef * ltype) list *)
           (* (arg_kind * pvar * pexp option) list *)
@@ -90,7 +106,7 @@ let heuristic_unparse cf lxp =
             Node (stypecons,
               Node (Symbol label, List.map pexp_u_formal_arg pfargs)
               :: List.map
-             (fun (name, types)
+              (fun (name, types)
               -> Node (Symbol (sexp_location loc, name),
                 List.map
                   (fun arg ->
@@ -104,7 +120,7 @@ let heuristic_unparse cf lxp =
                                          | Aerasable -> "_:::_"),
                               [Symbol id; loop t]))
                         types))
-                 (SMap.bindings ctors))
+                  (SMap.bindings ctors))
| Case (loc, target, bltp, branches, default)
           -> let bt = loop bltp in
@@ -161,9 +177,19 @@ let heuristic_unparse cf lxp =
                   [loop sl])
   in loop lxp
+(*
+and choice_find_opt lxp =
+  let res = List.filter (fun e -> e == OL.LMap.find_opt Elab.hc_elab_table lxp) Elab.hc_elab_table in
+  let s = ref DB.dsinfo in
+  List.nth res (Random.int (List.length res));
+  !s
+*)
+
+let print_heur_ctx_n (ctx : DB.elab_context) (ranges : (int * int) list) p n m  =
+  print_string (Fmt.make_title " LEXP CONTEXT : " );
+  print_string ("    =============================== Proba = 1/" ^ (string_of_int p) ^ " ==============================="); print_newline ();
+  print_string ("    =============================== Popu = " ^ (string_of_int m) ^ " ===============================") ; print_newline ();
-let print_heur_ctx_n (ctx : DB.elab_context) (ranges : (int * int) list) =
-  print_string (Fmt.make_title " LEXP CONTEXT ");
Fmt.make_rheader
     [
@@ -198,10 +224,10 @@ let print_heur_ctx_n (ctx : DB.elab_context) (ranges : (int * int) list) =
       lexp_print ty;
       print_newline();
-      let generate_population (le : lexp) n : sexp list =
+      let generate_population (le : lexp) p n : sexp list =
         let pop = ref [] in
-          for i = 1 to n do
-            let s = heuristic_unparse (fun _ -> Random.int i) le in
+          for _ = 1 to n do
+            let s = heuristic_unparse (Random.int p)  le in
             pop := s :: !pop
           done;
         !pop
@@ -211,10 +237,9 @@ let print_heur_ctx_n (ctx : DB.elab_context) (ranges : (int * int) list) =
         let le = (
           try Elab.infer_and_generalize_type ctx s (s, name)
           with
-          | e ->
-          raise e
+          | e -> raise e
         ) in
-       OL.conv_p (DB.ectx_to_lctx ctx) ty le
+        OL.conv_p (DB.ectx_to_lctx ctx) ty le
       in
let size (s : sexp) : int =
@@ -231,7 +256,7 @@ let print_heur_ctx_n (ctx : DB.elab_context) (ranges : (int * int) list) =
       in
let best_sexp (ss : sexp list) : sexp =
-        let res = List.filter (fun e -> fitness e == true) ss in
+        let res = List.filter (fun e -> fitness e) ss in
         let s = ref DB.dsinfo in
         let min = ref 0 in
         List.iter (
@@ -253,7 +278,7 @@ let print_heur_ctx_n (ctx : DB.elab_context) (ranges : (int * int) list) =
         !s;
       in
-      let _min_sexp res =
+      let min_sexp res =
         let s = ref DB.dsinfo in
         let min = ref 0 in
         List.iter (
@@ -264,7 +289,7 @@ let print_heur_ctx_n (ctx : DB.elab_context) (ranges : (int * int) list) =
         !s
       in
-      let select_sexp (ss : sexp list) : sexp list =
+      let _select_sexp (ss : sexp list) : sexp list =
         let res = ref [] in
         List.iter (
           fun e ->
@@ -288,7 +313,7 @@ let print_heur_ctx_n (ctx : DB.elab_context) (ranges : (int * int) list) =
               )
           | _ -> if Random.bool () then s1 else s2
         in
-        let _cross2 s1 s2 =
+        let cross2 s1 s2 =
           match s1, s2 with
           | Node (s1, ss1), Node (s2, ss2)
             -> Node ((if Random.bool () then s1 else s2),
@@ -301,44 +326,49 @@ let print_heur_ctx_n (ctx : DB.elab_context) (ranges : (int * int) list) =
if Random.bool ()
         then cross1 s1 s2
-        else cross1 s1 s2
+        else cross2 s1 s2
       in
-      let generate_parent (ss : sexp list) : sexp list =
-        let se = select_sexp ss in
+      let _generate_parent (ss : sexp list) : sexp list =
+        (* let se = select_sexp ss in *)
         let res = ref [] in
+        let s1 = (if best_sexp ss <> DB.dsinfo then best_sexp ss else min_sexp ss) in
         for _i = 1 to (List.length ss) do
-          let s1 = List.nth se (Random.int (List.length se)) in
-          sexp_print s1; print_newline ();
           let s2 = List.nth ss (Random.int (List.length ss)) in
-          sexp_print s2; print_newline ();
           let s = crossover s1 s2 in res := s :: !res;
-          sexp_print s;
-          print_newline ();
-          print_newline ();
         done;
         !res
       in
+      let gParentBS (ss : sexp list) : sexp list =
+        (* let se = select_sexp ss in *)
+        let res = ref [] in
+        let s1 = best_sexp ss in
+        for _ = 1 to (List.length ss) do
+          let s2 = List.nth ss (Random.int (List.length ss)) in
+          let s = crossover s1 s2 in res := s :: !res;
+        done;
+        !res
+      in
-      let algorithm lexp =
+       let algorithm lexp p n m =
         let loop ss =
           let res = ref [] in
-          for _i = 1 to 20 do
-            let se = generate_parent ss in
+          for _i = 1 to m do
+            let se = gParentBS ss in
             let s = best_sexp se in
             if s <> DB.dsinfo then
               res := s :: !res
             else
-              res := (max_sexp ss) :: !res;
+              if Random.bool () then res := (min_sexp ss) :: !res else res := (max_sexp ss) :: !res;
           done;
         !res
         in
-        let pop = generate_population lexp 10 in
+        let pop = generate_population lexp p n in
         let s = best_sexp pop in
         if s <> DB.dsinfo then
-          sexp_print s
+          let _ = print_newline () in sexp_print s;
         else
           let res = loop pop in
           let se = best_sexp res in
@@ -346,11 +376,10 @@ let print_heur_ctx_n (ctx : DB.elab_context) (ranges : (int * int) list) =
             sexp_print se
           else
             print_string " crossover --> "; sexp_print (max_sexp res);
-      in
-
-      algorithm ty;
+      in
+      algorithm ty p n m;
print_newline ();
       print_newline ();
@@ -380,8 +409,21 @@ let print_heur_ctx_n (ctx : DB.elab_context) (ranges : (int * int) list) =
(* Only print user defined variables *)
 let print_heur_ctx (lctx : DB.elab_context) : unit =
-  print_heur_ctx_n lctx [(0, M.length (DB.ectx_to_lctx lctx) - !builtin_size)]
+  print_heur_ctx_n lctx [(0, M.length (DB.ectx_to_lctx lctx) - !builtin_size)] 3 20 50
(* Dump the whole context *)
 let dump_heur_ctx (lctx : DB.elab_context) : unit =
-  print_heur_ctx_n lctx [(0, M.length (DB.ectx_to_lctx lctx))]
+  print_heur_ctx_n lctx [(0, M.length (DB.ectx_to_lctx lctx))] 3 20 50
+
+
+(* Only print user defined variables *)
+let test_print_heur_ctx (lctx : DB.elab_context) : unit =
+  for i = 2 to 10 do
+    print_heur_ctx_n lctx [(0, M.length (DB.ectx_to_lctx lctx) - !builtin_size)] i 500 50
+  done
+
+(* Dump the whole context *)
+let test_dump_heur_ctx (lctx : DB.elab_context) : unit =
+  for i = 2 to 10 do
+    print_heur_ctx_n lctx [(0, M.length (DB.ectx_to_lctx lctx))] i 500 50
+  done
=====================================
src/inverse_subst.ml
=====================================
@@ -197,15 +197,16 @@ exception Ambiguous
 (* Lookup variable i in s⁻¹ *)
 let rec lookup_inv_subst (i : db_index) (s : subst) : db_index
   = match s with
-  | (S.Identity o | S.Cons (_, _, o)) when i < o -> raise Not_invertible
+  (* | (S.Identity o | S.Cons (_, _, o)) when i < o -> raise Not_invertible *)
+  | (S.Identity o | S.Cons (_, _, o)) when i < o -> 1
   | S.Identity o -> i - o
   | S.Cons (e, s, o) when pred_var e (fun e -> get_var_db_index e = i - o)
     -> (try let i'' = lookup_inv_subst (get_var_db_index (get_var e)) s in
            assert (i'' != 0);
-           raise Ambiguous
-       with Not_invertible -> 0)
-  | S.Cons (e, s, o)
-    -> assert (match lexp_lexp' e with Var _ -> true | _ -> e = impossible);
+           raise Not_found
+       with Not_found -> 0)
+  | S.Cons (_e, s, o)
+    -> (* assert (match lexp_lexp' e with Var _ -> true | _ -> e = impossible); *)
       1 + lookup_inv_subst (i - o) s
(* When going under a binder, we have the rule
=====================================
src/lexp.ml
=====================================
@@ -356,8 +356,8 @@ let mkSLlub' (e1, e2) =
   match (lexp_lexp' e1, lexp_lexp' e2) with
   (* FIXME: This first case should be handled by calling `mkSLlub` instead!  *)
   | (SortLevel SLz, SortLevel l) | (SortLevel l, SortLevel SLz) -> l
-  | (SortLevel SLz, _) | (_, SortLevel SLz)
-    -> Log.log_fatal ~section:"internal" "lub of SLz"
+  | (SortLevel SLz, e) | (e, SortLevel SLz)
+    -> SLsucc (e, 0)
   | (SortLevel (SLsucc _), SortLevel (SLsucc _))
     -> Log.log_fatal ~section:"internal" "lub of two SLsucc"
   | ((SortLevel _ | Var _ | Metavar _ | Susp _),
=====================================
src/opslexp.ml
=====================================
@@ -962,7 +962,7 @@ and check'' erased ctx e =
and check' ctx e =
   let res = check'' DB.set_empty ctx e in
-    (Log.stop_on_error (); res)
+    ((* Log.stop_on_error (); *) res)
and check ctx e = check' ctx e
=====================================
src/pexp.ml
=====================================
@@ -48,9 +48,9 @@ let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) =
   match arg with
   | (Anormal, s, None) -> Symbol s
   | (ak, ((l,_) as s), t)
-    -> Node (Symbol (l, match ak with Aerasable -> ":::"
-                                   | Aimplicit -> "::"
-                                   | Anormal -> ":"),
+    -> Node (Symbol (l, match ak with Aerasable -> "_:::_"
+                                   | Aimplicit -> "_::_"
+                                   | Anormal -> "_:_"),
             [Symbol s; match t with Some e -> e
                                   | None -> Symbol (l, "_")])
=====================================
typer.sh
=====================================
@@ -9,6 +9,16 @@
# complete-filenames is useful for "%readfile ..." command
 # history-no-dupes just make it faster to search history with up and down key
-rlwrap --complete-filenames --history-no-dupes 1 ./_build/typer $*
+
+
+#rlwrap --complete-filenames --history-no-dupes 1 ./_build/typer $*
# if not specified history must be kept in "~/.typer_history"
+
+
+#
+
+# echo "%c" | OCAMLRUNPARAM=b dune exe ./typer.exe
+
+
+echo "%tc" | OCAMLRUNPARAM=b dune exe ./typer.exe > result_500.txt
\ No newline at end of file
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a1461ffe5326270999f6782632608d103...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a1461ffe5326270999f6782632608d103...
You're receiving this email because of your account on gitlab.com.





    