File tree Expand file tree Collapse file tree 5 files changed +8
-10
lines changed Expand file tree Collapse file tree 5 files changed +8
-10
lines changed Original file line number Diff line number Diff line change @@ -68,7 +68,7 @@ enumDecl1 name cons = IData EmptyFC (specified Public) Nothing dat
6868 enumName = UN $ Basic name
6969
7070 mkCon : String -> ITy
71- mkCon n = MkTy EmptyFC EmptyFC ( UN $ Basic n) (IVar EmptyFC enumName)
71+ mkCon n = MkTy EmptyFC (NoFC $ UN $ Basic n) (IVar EmptyFC enumName)
7272
7373 dat : Data
7474 dat = MkData EmptyFC enumName (Just (IType EmptyFC)) [] (map mkCon cons)
Original file line number Diff line number Diff line change @@ -246,6 +246,7 @@ deriveGeneral ns fs = do
246246 , "Record"
247247 , "Clause"
248248 , "Decl"
249+ , "IClaimData"
249250 ] [Generic', Eq', Ord']
250251```
251252
Original file line number Diff line number Diff line change @@ -667,3 +667,4 @@ getParamInfo' n = do
667667export % macro
668668getParamInfo : Name -> Elab ParamTypeInfo
669669getParamInfo = getParamInfo'
670+
Original file line number Diff line number Diff line change @@ -8,8 +8,7 @@ import Language.Reflection.Util
88
99ex1 : List Decl
1010ex1 =
11- [ IClaim
12- emptyFC
11+ [ IClaim $ NoFC $ MkIClaimData
1312 MW
1413 Private
1514 []
Original file line number Diff line number Diff line change @@ -73,15 +73,13 @@ ex9 =
7373
7474ex10 : List Decl
7575ex10 =
76- [ IClaim
77- emptyFC
76+ [ IClaim $ NoFC $ MkIClaimData
7877 MW
7978 Export
8079 [Inline ]
8180 (MkTy
8281 emptyFC
83- emptyFC
84- " test"
82+ (NoFC " test" )
8583 ( MkArg MW ExplicitArg Nothing (primVal (PrT IntType ))
8684 .-> primVal (PrT IntType )))
8785 , IDef
@@ -103,10 +101,9 @@ ex11 =
103101 []
104102 [ MkTy
105103 emptyFC
106- emptyFC
107- " A"
104+ (NoFC " A" )
108105 ( MkArg MW ExplicitArg Nothing (bindVar " t" )
109106 .-> var " Foo" .$ bindVar " t" )
110- , MkTy emptyFC emptyFC " B" (var " Foo" .$ bindVar " t" )
107+ , MkTy emptyFC ( NoFC " B" ) (var " Foo" .$ bindVar " t" )
111108 ])
112109 ]
You can’t perform that action at this time.
0 commit comments