order-of-equations.gr

-- gr --no-eval

data Vec (n : Nat) t where
  Nil  : Vec 0 t;
  Cons : t → Vec n t → Vec (n+1) t

mean : ∀ n : Nat . Vec (n + 1) Int → Int → Int → Int
mean (Cons x Nil) total n = div (x + total) n;
-- In this branch we need to know that xs can't be of type (Vec 0 _) for this to
-- type check. This follows from falling through the first equation.
mean (Cons x xs)  total n = mean xs (x + total) (n+1)

last : ∀ {a : Type, n : Nat} . (Vec (n+1) (a [0..1])) → a
last (Cons [x] Nil)   = x;
-- same here
last (Cons [_] xs)    = last xs