diff options
| author |  Nickolai Zeldovich <nickolai@csail.mit.edu> | 2015-07-16 18:24:19 -0400 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2015-09-03 18:11:32 +0200 |
| commit | c7fd3cb7945bcd385ace06f583d1b57681c8716d (patch) | |
| tree | efac429eaa0db1782ee5d08a464e46a6a1677f35 /pretyping | |
| parent | b06d3badbf5a8aa95e5150c2dc0b3fd44e1269ab (diff) | |
Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.v
The previous extraction of [Nat.div] for Haskell did not properly handle
divide-by-zero. Fix it by introducing an explicit [if] statement in the
generated Haskell code.
Also, introduce a similar extraction rule for [Nat.modulo], with the same
check for modulo-by-zero.
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions