Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Build error with Idris 1.3 #31

Closed
infinisil opened this issue Jun 22, 2018 · 1 comment
Closed

Build error with Idris 1.3 #31

infinisil opened this issue Jun 22, 2018 · 1 comment

Comments

@infinisil
Copy link

Reproducible with Nix:

$ nix-build https://github.com/nixos/nixpkgs/archive/a8c7103.tar.gz -A idrisPackages.bi
these derivations will be built:
  /nix/store/3cjip6k9ndqlsmdv1x3xmx7j5hqc79qk-bi-2018-01-17.drv
building '/nix/store/3cjip6k9ndqlsmdv1x3xmx7j5hqc79qk-bi-2018-01-17.drv'...
unpacking sources
unpacking source archive /nix/store/ngky5q8yzgghzfppb2sg1fzwyxzzj6r2-source
source root is source
patching sources
configuring
no configure script, doing nothing
building
Entering directory `./src'
Type checking ./Data/Bi.idr
Type checking ./Data/Util.idr
Type checking ./Data/Bip.idr
Type checking ./Data/Bip/AddMul.idr
Type checking ./Data/Bip/Iter.idr
./Data/Bip/Iter.idr:86:1-32:
   |
86 | iterInvariant f Inv  U    g x ix = g x ix
   | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking left hand side of iterInvariant:
When checking argument Inv to Data.Bip.Iter.iterInvariant:
        Inv is not a valid name for a pattern variable
builder for '/nix/store/3cjip6k9ndqlsmdv1x3xmx7j5hqc79qk-bi-2018-01-17.drv' failed with exit code 1
error: build of '/nix/store/3cjip6k9ndqlsmdv1x3xmx7j5hqc79qk-bi-2018-01-17.drv' failed
@clayrat
Copy link
Collaborator

clayrat commented Jun 22, 2018

Right, capital patterns are disallowed beginning from 1.3

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants