search

sbp / idris-bi

Idris Binary Integer Arithmetic, porting PArith, NArith, and ZArith from Coq
https://github.com/idris-lang/Idris-dev/issues/3976
36 stars 5 forks source link

Build error with Idris 1.3 #31

Closed infinisil closed 6 years ago

infinisil commented 6 years ago

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 commented 6 years ago

Right, capital patterns are disallowed beginning from 1.3