max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add Float.neg and casts

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-13 10:26:45 -08:00
parent b3703739af
commit e2773113a9
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/Data/Float.lean
View file

@ -35,6 +35,7 @@ instance : Inhabited Float := ⟨{ val := floatSpec.val }⟩
@[extern c inline "#1 - #2"] constant Float.sub : Float → Float → Float
@[extern c inline "#1 * #2"] constant Float.mul : Float → Float → Float
@[extern c inline "#1 / #2"] constant Float.div : Float → Float → Float
@[extern c inline "(- #1)"] constant Float.neg : Float → Float
set_option bootstrap.gen_matcher_code false
def Float.lt : Float → Float → Prop := fun a b =>
@ -49,6 +50,7 @@ instance : Add Float := ⟨Float.add⟩
instance : Sub Float := ⟨Float.sub⟩
instance : Mul Float := ⟨Float.mul⟩
instance : Div Float := ⟨Float.div⟩
instance : Neg Float := ⟨Float.neg⟩
instance : HasLess Float := ⟨Float.lt⟩
instance : HasLessEq Float := ⟨Float.le⟩
@ -69,6 +71,12 @@ instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
@[extern "lean_float_to_string"] constant Float.toString : Float → String
@[extern c inline "(uint8_t)#1"] constant Float.toUInt8 : Float → UInt8
@[extern c inline "(uint16_t)#1"] constant Float.toUInt16 : Float → UInt16
@[extern c inline "(uint32_t)#1"] constant Float.toUInt32 : Float → UInt32
@[extern c inline "(uint64_t)#1"] constant Float.toUInt64 : Float → UInt64
@[extern c inline "(size_t)#1"] constant Float.toUSize : Float → USize
instance : ToString Float where
toString := Float.toString