gistfile1.txt

$ 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 }
      }
}