Skip to content

Instantly share code, notes, and snippets.

@edwinb

edwinb/rational.idr

Created December 3, 2012 15:20
Show Gist options
  • Save edwinb/4195676 to your computer and use it in GitHub Desktop.
Save edwinb/4195676 to your computer and use it in GitHub Desktop.
Download ZIP
Rational
Raw
rational.idr
data Succ : Nat -> Set where
yes : Succ (S k)
data RationalP = RatP Nat Nat
data Rational : Set where
Rat : (num : Nat) -> (den : Nat) -> Succ den -> Rational
total toRational : RationalP -> Rational
toRational (RatP x y) = Rat x (S y) yes
total toRationalP : Rational -> RationalP
toRationalP (Rat x (S y) yes) = RatP x y
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment