raichoo

module Main

foo : (Int -> Int -> Int) -> IO Int
foo f = mkForeign (FFun "%0(1,2)" [FFunction FInt (FFunction FInt FInt)] FInt) f

main : IO ()
main = print !(foo (+))

-- Version with Le pretty!

raichoo

choice : (R : a -> a -> Type) ->
         ((n : a) -> (m : a ** R n m)) ->
         (f : (a -> a) ** (n : a) -> R n (f n))
choice R g = (\x => getWitness (g x) ** \y => getProof (g y))

raichoo

lem : (a : Type) -> Not (Not (Either a (Not a)))
lem a f = f (Right $ \x => f (Left x))

raichoo

module Choice where

record Σ(A : Set)(P : A → Set) : Set where
  field
    fst : A
    snd : P fst

choice : {A : Set}{R : A → A → Set} →
         ((n : A) → Σ A (λ m → R n m)) →
         Σ (A → A) (λ f → (

raichoo

check : (x : a) ->
        (f : a -> Bool) ->
        Either (f x = True) (f x = False)
check x f with (f x)
  | True  = Left refl
  | False = Right refl

raichoo

data Image : (a -> b) -> b -> Type where
  Im : {f : a -> b} -> (x : a) -> Image f (f x)

inv : (f : a -> b) -> (y : b) -> Image f y -> a
inv f y im with (im)
  inv f _ im | Im x = x

{-
  data Image{A B : Set}(f : A → B) : B → Set where
    image : (x : A) → Image f (f x)

raichoo

-- Only works in the REPL, compiled code explodes with SIGABRT
-- or SIGSEGV

-- Does not terminate
nats : Stream Nat
nats = 0 :: map (+1) nats

mapi : List a -> List (Nat, a)
mapi xs = mapi' nats xs
  where mapi' : Stream Nat -> List a -> List (Nat, a)

raichoo

%default total

cyclicAdd : Fin 4 -> Fin 4 -> Fin 4
cyclicAdd x y = head $ drop (finToNat x + finToNat y) fins
  where
    fins : Stream (Fin 4)
    fins = 0 :: 1 :: 2 :: 3 :: fins

raichoo

module Main

data FormatTy = FormatInt FormatTy
              | FormatChar Char FormatTy
              | FormatEnd

total
interpTy : FormatTy -> Type
interpTy (FormatInt ty)    = Int -> interpTy ty
interpTy (FormatChar x ty) = interpTy ty

raichoo

module WTypes where

import Level

data W(S : Set)(T : S → Set) : Set where
  _◁_ : (s : S) → (f : T s → W S T) → W S T

data ⊤ : Set where
  ⟨⟩ : ⊤