mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-01 16:12:26 +03:00
[ new ] Support reflecting on new intX types (#1642)
This commit is contained in:
parent
168a69bdcf
commit
39d596f3b9
@ -68,10 +68,14 @@ public export
|
||||
data Constant
|
||||
= I Int
|
||||
| BI Integer
|
||||
| B8 Int
|
||||
| B16 Int
|
||||
| B32 Int
|
||||
| B64 Integer
|
||||
| I8 Int8
|
||||
| I16 Int16
|
||||
| I32 Int32
|
||||
| I64 Int64
|
||||
| B8 Bits8
|
||||
| B16 Bits16
|
||||
| B32 Bits32
|
||||
| B64 Bits64
|
||||
| Str String
|
||||
| Ch Char
|
||||
| Db Double
|
||||
@ -79,6 +83,10 @@ data Constant
|
||||
|
||||
| IntType
|
||||
| IntegerType
|
||||
| Int8Type
|
||||
| Int16Type
|
||||
| Int32Type
|
||||
| Int64Type
|
||||
| Bits8Type
|
||||
| Bits16Type
|
||||
| Bits32Type
|
||||
|
Loading…
Reference in New Issue
Block a user