Skip to content

Commit 370a273

Browse files
danielkroenigallais
authored andcommitted
Inline Neg implementations
1 parent 1e8f9b3 commit 370a273

File tree

1 file changed

+11
-0
lines changed

1 file changed

+11
-0
lines changed

libs/prelude/Prelude/Num.idr

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,7 @@ Num Integer where
6868
(*) = prim__mul_Integer
6969
fromInteger = id
7070

71+
%inline
7172
public export
7273
Neg Integer where
7374
negate x = prim__sub_Integer 0 x
@@ -104,6 +105,7 @@ Num Int where
104105
(*) = prim__mul_Int
105106
fromInteger = prim__cast_IntegerInt
106107

108+
%inline
107109
public export
108110
Neg Int where
109111
negate x = prim__sub_Int 0 x
@@ -131,6 +133,7 @@ Num Int8 where
131133
(*) = prim__mul_Int8
132134
fromInteger = prim__cast_IntegerInt8
133135

136+
%inline
134137
public export
135138
Neg Int8 where
136139
negate x = prim__sub_Int8 0 x
@@ -158,6 +161,7 @@ Num Int16 where
158161
(*) = prim__mul_Int16
159162
fromInteger = prim__cast_IntegerInt16
160163

164+
%inline
161165
public export
162166
Neg Int16 where
163167
negate x = prim__sub_Int16 0 x
@@ -185,6 +189,7 @@ Num Int32 where
185189
(*) = prim__mul_Int32
186190
fromInteger = prim__cast_IntegerInt32
187191

192+
%inline
188193
public export
189194
Neg Int32 where
190195
negate x = prim__sub_Int32 0 x
@@ -212,6 +217,7 @@ Num Int64 where
212217
(*) = prim__mul_Int64
213218
fromInteger = prim__cast_IntegerInt64
214219

220+
%inline
215221
public export
216222
Neg Int64 where
217223
negate x = prim__sub_Int64 0 x
@@ -239,6 +245,7 @@ Num Bits8 where
239245
(*) = prim__mul_Bits8
240246
fromInteger = prim__cast_IntegerBits8
241247

248+
%inline
242249
public export
243250
Neg Bits8 where
244251
negate x = prim__sub_Bits8 0 x
@@ -266,6 +273,7 @@ Num Bits16 where
266273
(*) = prim__mul_Bits16
267274
fromInteger = prim__cast_IntegerBits16
268275

276+
%inline
269277
public export
270278
Neg Bits16 where
271279
negate x = prim__sub_Bits16 0 x
@@ -293,6 +301,7 @@ Num Bits32 where
293301
(*) = prim__mul_Bits32
294302
fromInteger = prim__cast_IntegerBits32
295303

304+
%inline
296305
public export
297306
Neg Bits32 where
298307
negate x = prim__sub_Bits32 0 x
@@ -320,6 +329,7 @@ Num Bits64 where
320329
(*) = prim__mul_Bits64
321330
fromInteger = prim__cast_IntegerBits64
322331

332+
%inline
323333
public export
324334
Neg Bits64 where
325335
negate x = prim__sub_Bits64 0 x
@@ -346,6 +356,7 @@ Num Double where
346356
(*) = prim__mul_Double
347357
fromInteger = prim__cast_IntegerDouble
348358

359+
%inline
349360
public export
350361
Neg Double where
351362
negate x = prim__negate_Double x

0 commit comments

Comments
 (0)