Skip to content

Instantly share code, notes, and snippets.

@anton-trunov

anton-trunov/MutInductiveExample.idr

Created February 10, 2017 12:55
Show Gist options
  • Save anton-trunov/0a702f954e620d309671c0e96cec89c6 to your computer and use it in GitHub Desktop.
Save anton-trunov/0a702f954e620d309671c0e96cec89c6 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
MutInductiveExample.idr
%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