Typer Janvier 2023

typer@iro.umontreal.ca

1 participants
3 discussions

[Git][monnier/typer][location-sinfo] Yes, accuracy score 100%
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

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

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

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Janvier 2023