git.iko.soy/Idris-dev
on master help sign in
Don't use a record for SourceLocation
commit0cc9d4c72d539dd130b0b16452c72d1a8834a315 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 15 Jan 2014, 17:03 (13 years ago) parentf24ae1d
1 file changed+1−1
compare with master
unifiedsplit
libs/base/Language/Reflection/Errors.idr+1−1
libs/base/Language/Reflection/Errors.idr+1−1
@@ -2,7 +2,7 @@ module Language.Reflection.Errors
22
33import Language.Reflection
44
5−record SourceLocation : Type where
5+data SourceLocation : Type where
66 FileLoc : (filename : String) -> (line : Int) -> (col : Int) -> SourceLocation
77
88%name SourceLocation loc