
--
-- Pattern matching and inductive families.
--

data Tree : Type -> Type where
  EAdd : Tree Integer -> Tree Integer -> Tree Integer
  EInt : Integer -> Tree Integer
  EFoo : (A:Type) -> A -> Tree A

eval : (B : Type) -> Tree B -> Tree B
eval _ t = case t of
		EAdd x y -> EInt (x+y)
		EInt i -> EInt i
		EFoo T x -> EFoo T x

strip : (B : Type) -> Tree B -> B
strip _ t = case t of
		EAdd x y -> x+y
		EInt i -> i
		EFoo _ x -> x

--
-- Subtyping
--

getX : { x : Integer } -> Integer
getX r = r.x

getY : { y : Integer } -> Integer
getY r = r.y

proj2 : (A:Type) -> (B:Type) -> (C:Type) -> (A -> B) -> (A -> C) -> A -> (B,C)
proj2 _ _ _ f g x = (f x, g x)

getXY : { x : Integer, y : Integer } -> (Integer,Integer)
getXY r = proj2 ? ? ? getX getY r
