You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This file has been removed and the functions have been placed in Typedefs.Typedefs. This has been done to satisfy nix to build typedefs, indeed, with the file and the imports present it would fail with the following error:
Type checking ./Typedefs/TermParse.idr
Can't find import Typedefs/Strings
builder for '/nix/store/z8s5px057m2gamxp9drh87741k3qihzv-idris-typedefs-core-dev.drv' failed with exit code 1
cannot build derivation '/nix/store/2r9jxqszndna5nyvmnqwbbymcnli3h74-idris-typedefs-examples-dev.drv': 1 dependencies couldn't be built
error: build of '/nix/store/2r9jxqszndna5nyvmnqwbbymcnli3h74-idris-typedefs-examples-dev.drv' failed
Those string-specific functions should return to Typedefs.Strings instead of polluting the Typedefs.Typedefs module.
The text was updated successfully, but these errors were encountered:
https://github.com/typedefs/typedefs/blob/fb909be7589509df0b78b29d43e35673f5177514/src/Typedefs/Strings.idr
This file has been removed and the functions have been placed in
Typedefs.Typedefs
. This has been done to satisfy nix to build typedefs, indeed, with the file and the imports present it would fail with the following error:Those string-specific functions should return to
Typedefs.Strings
instead of polluting theTypedefs.Typedefs
module.The text was updated successfully, but these errors were encountered: