Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
$ echo "../dhall-bhat/Field/terms.dhall
Type
../dhall-bhat/Category/Monoidal/Set/cartesian
../dhall-bhat/Function/category
../dhall-bhat/Tuple/functor/pair
(./Ratio/Type ./Int/Type)
(./Ratio/field ./Int/Type ./Int/ring)
" | /nix/store/d1mk2rhfrm9ml3m3hyxdala9s0aygvcd-dhall-1.18.0/bin/dhall
{ add =
λ ( t
: { _1 :
{ denominator :
{ magnitude : Natural, positive : Bool }
, numerator :
{ magnitude : Natural, positive : Bool }
}
, _2 :
{ denominator :
{ magnitude : Natural, positive : Bool }
, numerator :
{ magnitude : Natural, positive : Bool }
}
}
)
→ { denominator =
{ magnitude =
t._1.denominator.magnitude * t._2.denominator.magnitude
, positive =
t._1.denominator.positive
}
, numerator =
{ magnitude =
t._1.numerator.magnitude * t._2.denominator.magnitude
+ t._1.denominator.magnitude * t._2.numerator.magnitude
, positive =
t._1.numerator.positive
}
}
, divide =
λ ( x
: { _1 :
{ denominator :
{ magnitude : Natural, positive : Bool }
, numerator :
{ magnitude : Natural, positive : Bool }
}
, _2 :
{ denominator :
{ magnitude : Natural, positive : Bool }
, numerator :
{ magnitude : Natural, positive : Bool }
}
}
)
→ { denominator =
{ magnitude =
x._1.denominator.magnitude * x._2.numerator.magnitude
, positive =
x._1.denominator.positive
}
, numerator =
{ magnitude =
x._1.numerator.magnitude * x._2.denominator.magnitude
, positive =
x._1.numerator.positive
}
}
, multiply =
λ ( t
: { _1 :
{ denominator :
{ magnitude : Natural, positive : Bool }
, numerator :
{ magnitude : Natural, positive : Bool }
}
, _2 :
{ denominator :
{ magnitude : Natural, positive : Bool }
, numerator :
{ magnitude : Natural, positive : Bool }
}
}
)
→ { denominator =
{ magnitude =
t._1.denominator.magnitude * t._2.denominator.magnitude
, positive =
t._1.denominator.positive
}
, numerator =
{ magnitude =
t._1.numerator.magnitude * t._2.numerator.magnitude
, positive =
t._1.numerator.positive
}
}
, one =
λ(_ : {})
→ { denominator =
{ magnitude = 1, positive = True }
, numerator =
{ magnitude = 1, positive = True }
}
, subtract =
λ ( x
: { _1 :
{ denominator :
{ magnitude : Natural, positive : Bool }
, numerator :
{ magnitude : Natural, positive : Bool }
}
, _2 :
{ denominator :
{ magnitude : Natural, positive : Bool }
, numerator :
{ magnitude : Natural, positive : Bool }
}
}
)
→ { denominator =
{ magnitude =
x._1.denominator.magnitude * x._2.denominator.magnitude
, positive =
x._1.denominator.positive
}
, numerator =
{ magnitude =
x._1.numerator.magnitude * x._2.denominator.magnitude
+ x._1.denominator.magnitude * x._2.numerator.magnitude
, positive =
x._1.numerator.positive
}
}
, zero =
λ(_ : {})
→ { denominator =
{ magnitude = 1, positive = True }
, numerator =
{ magnitude = 0, positive = True }
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.