Typer
Discussions par mois
- ----- 2026 -----
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2025 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2024 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2023 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2022 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2021 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2020 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2019 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2018 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2017 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2016 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
Janvier 2023
- 1 participants
- 3 discussions
[Git][monnier/typer][location-sinfo] Yes, accuracy score 100%
by Ismaila FALL (@Fallismaila) 27 Jan '23
by Ismaila FALL (@Fallismaila) 27 Jan '23
27 Jan '23
Ismaila FALL pushed to branch location-sinfo at Stefan / Typer
Commits:
68c2576e by Fallismaila at 2023-01-27T05:16:40+00:00
Yes, accuracy score 100%
- - - - -
30 changed files:
- − .idea/encodings.xml
- − .idea/vcs.xml
- − .idea/workspace.xml
- − _build/.aliases/default/btl/all-00000000000000000000000000000000
- − _build/.aliases/default/btl/typer_stdlib-00000000000000000000000000000000
- − _build/.aliases/default/btl/typer_stdlib-894e20e3a05c970afce59190ae53ce77
- − _build/.aliases/default/doc/all-00000000000000000000000000000000
- − _build/.aliases/default/doc/formal/all-00000000000000000000000000000000
- − _build/.aliases/default/emacs/all-00000000000000000000000000000000
- − _build/.aliases/default/samples/all-00000000000000000000000000000000
- − _build/.aliases/default/samples/typer_samples-00000000000000000000000000000000
- − _build/.aliases/default/samples/typer_samples-894e20e3a05c970afce59190ae53ce77
- − _build/.aliases/default/src/old/all-00000000000000000000000000000000
- − _build/.aliases/default/tests/runtest-00000000000000000000000000000000
- − _build/.aliases/default/tests/runtest-01fdccf548462383a9561aecdd756b89
- − _build/.aliases/default/tests/runtest-20dc196fb8ccf643be5a5939c7681050
- − _build/.aliases/default/tests/runtest-3475e63958295e1170ae43a6e2288f7d
- − _build/.aliases/default/tests/runtest-42138be92a6dec907b00aa6c88b5c239
- − _build/.aliases/default/tests/runtest-7590510b5dfec4d41c8197e4a3b33cf9
- − _build/.aliases/default/tests/runtest-866a3b05386e78352d5b65dc32fdc35e
- − _build/.aliases/default/tests/runtest-aab4b3e83a782d18085646303013a91e
- − _build/.aliases/default/tests/runtest-af0fbd98ed92a2210cdc516e9a252311
- − _build/.aliases/default/tests/runtest-df403c4ff7d394eb7dd6db556b4a75e4
- − _build/.aliases/default/tests/runtest-e08b364de551ff675127d711315beae8
- − _build/.aliases/default/tests/runtest-f36943f88e093ddc9d7f85b013f2c041
- − _build/.aliases/default/tests/runtest-f6c70f09aa65aa5cf3c0877b3cf4f21b
- − _build/.aliases/default/tests/runtest-ff30713b4b87e30d714cbf34653ddbe9
- − _build/.db
- − _build/.digest-db
- − _build/.filesystem-clock
The diff was not included because it is too large.
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/68c2576e4ace5ebbe75f8950efc0c14a2…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/68c2576e4ace5ebbe75f8950efc0c14a2…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][location-sinfo] Yes, accuracy score 100%
by Ismaila FALL (@Fallismaila) 27 Jan '23
by Ismaila FALL (@Fallismaila) 27 Jan '23
27 Jan '23
Ismaila FALL pushed to branch location-sinfo at Stefan / Typer
Commits:
a34635da by Fallismaila at 2023-01-27T05:10:48+00:00
Yes, accuracy score 100%
- - - - -
30 changed files:
- −
- − .gitignore
- + .idea/encodings.xml
- + .idea/vcs.xml
- + .idea/workspace.xml
- + _build/.aliases/default/btl/all-00000000000000000000000000000000
- + _build/.aliases/default/btl/typer_stdlib-00000000000000000000000000000000
- _) → _build/.aliases/default/btl/typer_stdlib-894e20e3a05c970afce59190ae53ce77
- + _build/.aliases/default/doc/all-00000000000000000000000000000000
- + _build/.aliases/default/doc/formal/all-00000000000000000000000000000000
- + _build/.aliases/default/emacs/all-00000000000000000000000000000000
- + _build/.aliases/default/samples/all-00000000000000000000000000000000
- + _build/.aliases/default/samples/typer_samples-00000000000000000000000000000000
- + _build/.aliases/default/samples/typer_samples-894e20e3a05c970afce59190ae53ce77
- + _build/.aliases/default/src/old/all-00000000000000000000000000000000
- + _build/.aliases/default/tests/runtest-00000000000000000000000000000000
- + _build/.aliases/default/tests/runtest-01fdccf548462383a9561aecdd756b89
- + _build/.aliases/default/tests/runtest-20dc196fb8ccf643be5a5939c7681050
- + _build/.aliases/default/tests/runtest-3475e63958295e1170ae43a6e2288f7d
- + _build/.aliases/default/tests/runtest-42138be92a6dec907b00aa6c88b5c239
- + _build/.aliases/default/tests/runtest-7590510b5dfec4d41c8197e4a3b33cf9
- + _build/.aliases/default/tests/runtest-866a3b05386e78352d5b65dc32fdc35e
- + _build/.aliases/default/tests/runtest-aab4b3e83a782d18085646303013a91e
- + _build/.aliases/default/tests/runtest-af0fbd98ed92a2210cdc516e9a252311
- + _build/.aliases/default/tests/runtest-df403c4ff7d394eb7dd6db556b4a75e4
- + _build/.aliases/default/tests/runtest-e08b364de551ff675127d711315beae8
- + _build/.aliases/default/tests/runtest-f36943f88e093ddc9d7f85b013f2c041
- + _build/.aliases/default/tests/runtest-f6c70f09aa65aa5cf3c0877b3cf4f21b
- + _build/.aliases/default/tests/runtest-ff30713b4b87e30d714cbf34653ddbe9
- + _build/.db
The diff was not included because it is too large.
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a34635da54c3245eb3948e210243c2742…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a34635da54c3245eb3948e210243c2742…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][location-sinfo] 2 commits: save results AG
by Ismaila FALL (@Fallismaila) 10 Jan '23
by Ismaila FALL (@Fallismaila) 10 Jan '23
10 Jan '23
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/a1461ffe5326270999f6782632608d10…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a1461ffe5326270999f6782632608d10…
You're receiving this email because of your account on gitlab.com.
1
0