5 ms·
There [0]: the GCD m n d type proves that the greatest common divisor of m and n is d. [0] http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/GCD.agda http
by pka 10y ago
There [0]: the GCD m n d type proves that the greatest common divisor of m and n is d.
[0] http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/GCD.agda http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/GCD.a...
- willtim 10y agoThis is a great example. I also recall seeing refinement types (Liquid Haskell) used to prove termination of Euclids GCD.
- kazinator 10y agoFor all I know, the GCD function buried in that gobbledygook could actually be calculating the LCM, and the proof could be of that.
- pka 10y agoFor all I know Agreed.