swh:1:snp:aeaf3dbb58f5be84b565e73b5ade1503ee8cb6d6
Tip revision: b6407e0f026cf5491ca5ed0a35ea5cf316ebe8ca authored by Anish Tondwalkar on 21 May 2021, 03:15:25 UTC
formatted for submission
formatted for submission
Tip revision: b6407e0
recursion.hs
measure mNil :: List [>Int] -> Bool
measure mCons :: List [>Int] -> Bool
measure mLength :: List [>Int] -> Int
measure not :: Bool -> Bool
empty as x:(List >Int) ->
{v: Bool | (v == mNil x) /\ (v == not (mCons x)) /\ (v == (mLength x == 0))}
empty = (0)
nil as {v: List >Int | (mNil v) /\ (mLength v = 0) /\ (not (mCons v))}
nil = (0)
cons as x:Int -> xs:(List >Int) ->
{v: List >Int | (mCons v) /\ (mLength v = mLength xs + 1) /\ (not (mNil v))}
cons = (0)
first as {v: List >Int | mCons v} -> Int
first = (0)
rest as rs:{v: List >Int | mCons v}
-> {v: List >Int | mLength v + 1 == mLength rs }
rest = (0)
append :: xs:(List >Int)
-> ys:(List >Int)
-> {v: List >Int | mLength v = (mLength xs) + (mLength ys)}
append = \xs -> \ys ->
if empty xs
then ys
else cons (first xs) (append (rest xs) ys)