xekoukou

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

xekoukou

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

xekoukou

module Main

%default total

data Test : Type where
  OneC : Nat -> Test
  TwoC : String -> Test

funT : Test -> Type
funT (OneC (S k)) = String

xekoukou

module LinLogic


import public Syntax.PreorderReasoning
import public Data.Vect
import public Data.HVect
import public Prelude.Uninhabited

%access public export

xekoukou

module LinLogic


import public Syntax.PreorderReasoning
import public Data.Vect
import public Data.HVect
import public Prelude.Uninhabited

%access public export

xekoukou

module LinLogic


import public Syntax.PreorderReasoning
import public Data.Vect
import public Data.HVect
import public Prelude.Uninhabited

%access public export

xekoukou

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

xekoukou

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

xekoukou

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 ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>

xekoukou

-- `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