Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
%default total
mutual
data First = FirstSimple | FirstSecond Second
data Second = SecondSimple | SecondFirst ListFirst
data ListFirst = NilFirst | ConsFirst First ListFirst
mutual
calculateFirst : First -> Nat
calculateFirst FirstSimple = 1
calculateFirst (FirstSecond x) = calculateSecond x
calculateSecond : Second -> Nat
calculateSecond SecondSimple = 2
calculateSecond (SecondFirst xs) = calculateListFirst xs
calculateListFirst : ListFirst -> Nat
calculateListFirst NilFirst = 0
calculateListFirst (ConsFirst h tl) = calculateFirst h + calculateListFirst tl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment