This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
let pack ls = | |
let buf = Buffer.create (List.length ls) in | |
let e = Uutf.encoder utf8 (`Buffer buf) | |
in let rec loop ls = match ls with | |
| [] -> Buffer.contents buf | |
| (c :: ls) -> print_string (Buffer.contents buf) ; let _ = Uutf.encode e (`Uchar c) in () ; loop ls | |
in loop ls |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
opam install malfunction | |
=-=- Synchronising pinned packages =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= | |
[malfunction] https://github.com/stedolan/malfunction downloaded | |
The following actions will be performed: | |
∗ install zarith 1.7 [required by malfunction] | |
∗ install malfunction 0.2.1* | |
===== ∗ 2 ===== | |
Do you want to continue ? [Y/n] y |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module LinLogic | |
import public Syntax.PreorderReasoning | |
import public Data.Vect | |
import public Data.HVect | |
import public Prelude.Uninhabited | |
%access public export |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module LinLogic | |
import public Syntax.PreorderReasoning | |
import public Data.Vect | |
import public Data.HVect | |
import public Prelude.Uninhabited | |
%access public export |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module LinLogic | |
import public Syntax.PreorderReasoning | |
import public Data.Vect | |
import public Data.HVect | |
import public Prelude.Uninhabited | |
%access public export |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Main | |
%default total | |
data Test : Type where | |
OneC : Nat -> Test | |
TwoC : String -> Test | |
funT : Test -> Type | |
funT (OneC (S k)) = String |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
LDecl MkUnit LConstructor 0 0 | |
LDecl io_bind LFun [] [{e0} {e1} {e2} {e3} {e4} w ] | |
LApp False | |
LV Glob {io_bind2} [ | |
LV Glob {e0} | |
LV Glob {e1} | |
LV Glob {e2} | |
LV Glob {e3} | |
LV Glob {e4} | |
LV Glob w |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Main | |
%default total | |
data Chat_State : Nat -> Type where | |
Ask_Name : Chat_State 3 | |
Get_Name : (List String) -> Chat_State 2 | |
Greet : (List String) -> Chat_State 1 | |
End : (List String) -> Chat_State 0 |
NewerOlder