Skip to content

Commit f3d62b8

Browse files
jfdmgallais
authored andcommitted
[ fix ] stuck elaboration in parser library.
The type of the `Text.Parser` function `count` requires access to the `min` function of `Data.Nat`. If `Data.Nat` has not been imported in your parser module, then usages of `count` will fail to elaborate correctly. Thus, one can see errors of the form: ``` Error: While processing right hand side of header. Can't solve constraint between: isSucc (min (between 1 6)) || Delay ?c2 and True. ``` This fix makes the import of `Data.Nat` public.
1 parent 0d6e89a commit f3d62b8

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

libs/contrib/Text/Parser.idr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
module Text.Parser
22

33
import Data.Bool
4-
import Data.Nat
4+
import public Data.Nat
55
import public Data.List1
66

77
import public Text.Parser.Core

0 commit comments

Comments
 (0)