diff options
| author | Pierre Roux | 2018-08-28 18:56:07 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:35 +0100 |
| commit | d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab (patch) | |
| tree | 9cc9b39b16849ed839f4adf7b19e3d3291f7dd98 /theories/Floats/FloatClass.v | |
| parent | 79605dabb10e889ae998bf72c8483f095277e693 (diff) | |
Implement classify on primitive float
Diffstat (limited to 'theories/Floats/FloatClass.v')
| -rw-r--r-- | theories/Floats/FloatClass.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Floats/FloatClass.v b/theories/Floats/FloatClass.v new file mode 100644 index 0000000000..3241035aef --- /dev/null +++ b/theories/Floats/FloatClass.v @@ -0,0 +1,2 @@ +Inductive float_class : Set := + | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN. |