raichoo

total
isElem' : DecEq a => (e : a) -> (t : Tree a) -> Dec (IsElem e t)
isElem' x Leaf = No $ \p => noElemInLeaf x p
  where
    total
    noElemInLeaf : (x : a) -> IsElem x Leaf -> _|_
    noElemInLeaf x Here impossible

isElem' x (Branch l y r) with (decEq x y)
  isElem' x (Branch l x r) | Yes refl = Yes Here

raichoo

var __IDRLT__APPLY65610 = function(mfn0,marg0){
  return new __IDRRT__Cont(function(){
    return __IDRRT__print(mfn0.vars[0])
  })
}

var __IDRLT__APPLY65611 = function(mfn0,marg0){
  return new __IDRRT__Cont(function(){
    return __IDR__mAPPLY0(mfn0.vars[1],marg0)
  })

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