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 |
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 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
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
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
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
apostolis@Geraki:~/WorkSpace$ opam install uunf uucp uutf | |
[NOTE] Package uutf is already installed (current version is 1.0.1). | |
[NOTE] Package uucp is already installed (current version is 11.0.0). | |
The following actions will be performed: | |
∗ install uunf 11.0.0 | |
↻ recompile uucp 11.0.0 | |
===== ∗ 1 ↻ 1 ===== | |
Do you want to continue? [Y/n] y | |
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> |
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
-- `accepts`, in defunctionalized style: | |
accepts :: State -> String -> Bool | |
accepts S0 ('a':xs) = accepts S1 xs | |
accepts S0 ('b':xs) = accepts S2 xs | |
accepts S1 ('a':xs) = accepts S2 xs | |
accepts S1 ('b':xs) = accepts S0 xs | |
accepts S2 ('a':xs) = accepts S0 xs | |
accepts S2 ('b':xs) = accepts S2 xs | |
accepts S2 _ = True | |
accepts _ _ = False |
OlderNewer