hughfdjackson

sPlusAssoc : (m, n: Nat) -> S (m + n) = plus m (S n)
sPlusAssoc Z     n = refl
sPlusAssoc (S m) n = rewrite sPlusAssoc m n in refl
 
total concat : Vect n a -> Vect m a -> Vect ((replace sPlusAssoc) (plus m n)) a
concat (x :: xs) ys = x :: (concat xs ys)
concat nil       ys = ys

hughfdjackson

- tutorial.idr line 16 col 9:
     When elaborating right hand side of prepend:
     Can't unify
             Vect (S (m + n)) a
     with
             Vect (plus m (S n)) a
     
     Specifically:
             Can't unify
                     S (m + n)

hughfdjackson

module reverse

total snoc : Vect n a -> a -> Vect (S n) a
snoc Nil        a = a :: Nil
snoc (x :: xs)  a = x :: (xs `snoc` a)     

total reverse' : Vect n a -> Vect n a
reverse' (x :: xs) = (reverse' xs) `snoc` x
reverse' Nil       = Nil

hughfdjackson

snoc' : Vect n a -> a -> Vect (S n) a
snoc' (x :: Nil) a = x :: a :: Nil
snoc' (x :: xs)  a = x :: (snoc' xs a)

hughfdjackson

- + Errors (1)
 `-- tutorial.idr line 41 col 5:
     When elaborating right hand side of snoc:
     Can't unify
             Vect (n + 1) a
     with
             Vect (S n) a
     
     Specifically:
             Can't unify

hughfdjackson

import List (foldl, map)

data Acceptable = X { x: Int } | XY { y: Int, x: Int }

list : [Acceptable]
list = [X { x = 10 }, XY { x = 20, y = 10 }]

type Xable a = { a | x: Int }

sumX : [Xable a] -> Int

hughfdjackson

data Acceptable = Xable { x: Int } | Yable { y: Int }


list : [Acceptable]
list = [Xable { x = 10 }, Yable { y = 10 }]

main = asText  list

hughfdjackson

type Xable a = { a | x: Int }
main = asText [Xable { x = 10, y = 20 }, { x = 10 }]

hughfdjackson

module Scene where

type Camera = {}

-- entity is a thing that can be rendered and updated
type Entity e = { e |
  render: e -> Element,
  update: e -> e
}

hughfdjackson

type State = { prev: Int, curr: Int }

tick = every second

updateState timestamp state = { state | prev <- state.curr, curr <- timestamp } 

main = lift asText <| foldp updateState { prev = 0, curr = 0 } tick