ChristopherKing42

--Roughly based on https://github.com/Gabriel439/Haskell-Morte-Library/blob/master/src/Morte/Core.hs by Gabriel Gonzalez et al.

data Expr = Star | Box | Var Int | Lam Int Expr Expr | Pi Int Expr Expr | App Expr Expr deriving (Show, Eq)

subst v e (Var v')       | v == v' = e
subst v e (Lam v' ta b ) | v == v' = Lam v' (subst v e ta)            b
subst v e (Lam v' ta b )           = Lam v' (subst v e ta) (subst v e b )
subst v e (Pi  v' ta tb) | v == v' = Pi  v' (subst v e ta)            tb
subst v e (Pi  v' ta tb)           = Pi  v' (subst v e ta) (subst v e tb)
subst v e (App f a     )           = App    (subst v e f ) (subst v e a )

MarcelineVQ

module Network.Curl.Prim

import Data.Bytes.Lazy

import Control.App
import Network.Curl.Types
import Network.Curl.Option

import Data.Bytes.Strict
import Data.Word.Word8

MarcelineVQ

import Data.Buffer

-- Redefining this here to modify it
%foreign "scheme:blodwen-new-buffer"
prim_newBuffer' : Int -> PrimIO Buffer

export
newBuffer' : HasIO io => (bytes : Int) -> io Buffer
newBuffer' size = primIO $ prim_newBuffer' size
-- No Maybe, if we can't allocate memory then die.