Skip to content

Instantly share code, notes, and snippets.

@5outh

5outh/Rational.idr

Created May 12, 2016 23:16
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save 5outh/72ac7d886c0d05df6b98871c392843c7 to your computer and use it in GitHub Desktop.
Save 5outh/72ac7d886c0d05df6b98871c392843c7 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Rational.idr
data Rational : Nat -> Nat -> Type where
MkRational : (a : Nat) -> (b : Nat) -> Rational a b
MultRat : Rational a b -> Rational c d -> Rational (a*c) (b*d)
DivRat : Rational a b -> Rational c d -> Rational (a*d) (b*c)
AddRat : Rational a b -> Rational c d -> Rational (a*d + b*c) (b*d)
Simplify : Rational a b -> Rational (divNat a (gcd a b)) (divNat b (gcd a b))
||| λΠ> :t Simplify (DivRat (MkRational 770 30) (MkRational 3 4))
||| Simplify (DivRat (MkRational 770 30) (MkRational 3 4)) : Rational 308 9
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment