elliotpotts

okay I'm a little bit confused

[11:47] 
I have a metavariable `succ = \n. \s. \z. s ((n s) z)`

[11:47] 
and I want to apply it to the metavariable `zero = \s. \z. z`

[11:47] 
so I would have

elliotpotts

type Var = String
type Z = Int
type State = Var -> Z

emptyState :: State
emptyState = const 0

assign :: State -> Var -> Z -> State
assign oldst name var x = if x == name then value else oldst x

elliotpotts

parity_local :: String
parity_local = "begin \n\
               \    var y := 2034; \n\
               \    proc iseven is begin \n\
               \        if y = 0 then \n\
               \            mod2 := 0 \n\
               \        else \n\
               \            y := y - 1; \n\
               \            call isodd \n\
               \    end; \n\

elliotpotts

fix :: (a -> a) -> a
fix f = f (fix f)

fib :: (Int -> Int) -> Int -> Int
fib rec n = case n of
              0 -> 1
              1 -> 1
              x -> (rec (x - 1)) + (rec (x - 2))

fib' :: Int -> Int

elliotpotts

data BlackHole : Type where
  MkBlackHole : (a -> BlackHole) -> BlackHole

fix : (a -> a) -> a
fix f = f (fix f)

b : BlackHole
b = MkBlackHole {a = fixt} (fix MkBlackHole) where
  fixt : Type
  fixt = fixt -> BlackHole

elliotpotts

from itertools import groupby

gallery_rows = [(0, "holiday"), (1, "nonempty"), (2, "christmas")]
images_rows = [(0, "beach.jpg"), (0, "pool.jpg"), (1, "removeme.jpg"), (2, "santa.jpg")]
images_grouped = groupby(images_rows, lambda x: x[0])

objs = []
for gallery in gallery_rows:
    obj = {}
    obj["name"] = gallery[1]

elliotpotts

import Data.Vect
import Data.List.Quantifiers

Alphabet : Vect 26 Char
Alphabet = ['a','b','c','d','e','f','g',
            'h','i','j','k','l','m','n',
            'o','p','q','r','s','t','u',
            'v','w','x','y','z']
Digits : Vect 10 Char
Digits = ['0','1','2','3','4','5','6','7','8','9']

elliotpotts

import sqlalchemy
import sqlalchemy.ext.declarative
from sqlalchemy import Column, ForeignKey, Integer, String
from sqlalchemy.orm import relationship

engine = sqlalchemy.create_engine("...")
Base = sqlalchemy.ext.declarative.declarative_base()
Session = sqlalchemy.orm.sessionmaker(bind=engine)

class Image(Base):

elliotpotts

data General : (phi : Type) -> (r : phi -> Type) -> (a : Type) -> Type where
  Here : a -> General phi r a
  Request : (ix : phi) -> (k : r ix -> General phi r a) -> General phi r a

implementation Functor (General phi r) where
  map f (Here x) = Here (f x)
  map f (Request ix k) = Request ix (\j => map f $ k j)

implementation Applicative (General phi r) where
  pure = Here

elliotpotts

data General : (phi : Type) -> (r : phi -> Type) -> (a : Type) -> Type where
  Here : a -> General phi t a
  Request : (ix : phi) -> (k : t ix -> General phi t a) -> General phi t a

implementation Functor (General phi t) where
  map f (Here x) = Here (f x)
  map f (Request ix k) = Request ix (\j => map f $ k j)

implementation Applicative (General phi t) where
  pure = Here