append.hs
measure mNil :: List [] -> Bool
measure mCons :: List [] -> Bool
measure mLength :: List [] -> Int
empty as rforall a. x:(List <a) -> {v: Bool | v == mNil x}
empty = (0)
nil as rforall a. {v: List <a | (mNil v) /\ (mLength v = 0)}
nil = (0)
cons as rforall a. x:a -> xs:(List <a) -> {v: List <a | (mCons v) /\ (mLength v = mLength xs + 1)}
cons = (0)
first as rforall a. {v: List <a | mCons v} -> a
first = (0)
rest as rforall a. {v: List <a | mCons v} -> List <a
rest = (0)
append :: rforall a. xs:(List <a) -> ys:(List <a) -> {v: List <a | mLength v = mLength xs}
append = \xs -> \ys ->
if empty xs
then ys
else cons (first xs) (append (rest xs) ys)