Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-07-30 00:50 8f654965

View on Github →

feat(data/fp): first pass at a floating point model Hopefully this will be eventually moved to init so it can get a native representation.

Estimated changes

Created data/fp/basic.lean

added def fp.div_nat_lt_two_pow

added def fp.emax

added def fp.emin

added def fp.float.default_nan

added def fp.float.is_finite

added theorem fp.float.zero.valid

added def fp.float.zero

added inductive fp.float

added structure fp.nan_pl

added def fp.prec

added inductive fp.rmode

added def fp.shift2

added def fp.to_rat

added def fp.valid_finite