idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 12:42:02 +03:00
Code Issues Projects Releases Wiki Activity

Fix typo

Browse Source
This commit is contained in:
Zoe Stafford 2023-03-05 11:06:05 +00:00
parent 7972c6acbd
commit 5e3b9634fe
No known key found for this signature in database
GPG Key ID: B461D9E741A66EB0
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/Compiler/Common.idr
View File

@ -561,7 +561,8 @@ record ConstantPrimitives' str where
intToInt : IntKind -> IntKind -> str -> Core str
public export
ConstantPrimitives : Type = ConstantPrimitives' String
ConstantPrimitives : Type
ConstantPrimitives = ConstantPrimitives' String
||| Implements casts from and to integral types by using
||| the implementations from the provided `ConstantPrimitives`.