search

sbp / idris-bi

Idris Binary Integer Arithmetic, porting PArith, NArith, and ZArith from Coq
https://github.com/idris-lang/Idris-dev/issues/3976
36 stars 5 forks source link

Port QArith #9

Open sbp opened 7 years ago

sbp commented 7 years ago

Whilst I only envisaged porting the P, N, and Z arithmetics from Coq, it might be nice to go for full-on completion and port QArith too. I'm not sure what the type should be, but probably something like this:

record Biq where
  constructor Ratio
  numerator: Biz
  denominator: Bip

The constructor could be Rational instead of Ratio, though by convention it should really be MkBiq. Coq uses num and den for the field names. I don't like "num", but perhaps n and d, or numer and denom would be okay.

sbp commented 7 years ago

Just to make things extra confusing, Coq also immediately defines a way to get the denominator as a positive Z, i.e. BizP in our nomenclature, which is then apparently used quite a lot.

clayrat commented 7 years ago

Sounds good, but we should probably finish P/N/Z first :)