on master help sign in
Add more rules for primitives.
059a39fMatus Tejiscak
src/Idris/Erasure.hs+4
@@ -110,6 +110,10 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
110 , it "prim__sltBigInt" [0,1]
110 , it "prim__sltBigInt" [0,1]
111 , it "prim__sltChar" [0,1]
111 , it "prim__sltChar" [0,1]
112 , it "prim__toStrInt" [0,1]
112 , it "prim__toStrInt" [0,1]
113+ , it "prim__addInt" [0,1]
114+ , it "prim__eqInt" [0,1]
115+ , it "prim__sltInt" [0,1]
116+ , it "prim__subInt" [0,1]
113 , mn "__MkPair" [0,1]
117 , mn "__MkPair" [0,1]
114 ]
118 ]
115 ]
119 ]