Frédéric Blanqui
Frédéric Blanqui
The problem is in https://github.com/Deducteam/lambdapi/blob/08755211c073f4216c34f8dd7864ce3b874415b4/src/core/eval.ml#L221-L227
Note that this kind of unification rule could be used to invert π:Prop → TYPE: ``` rule π (∀ x, $f[x]) ↪ Π x, π $f[x]; unif_rule π $p ≡...
The problem is that an extra pattern variable must be replaced by a fresh metavariable but, to create a fresh metavariable, you need to give it a type. The type...
Ouah. That's great @gares . Thank you for digging into the code of Lambdapi !
Yes: ``` 18:39 ~/lambdapi (elpi) make sanity_check In src/core/ctxt.ml, line 12 more than 78 characters... In src/core/elpi_lambdapi.ml, line 53 more than 78 characters... In src/core/elpi_lambdapi.ml, line 95 more than 78...
Well, 79>78 indeed ;-) But that's strange we do not get the same files! Do you use gawk? I have `GNU Awk 4.1.4`. Could you please give the complete result...
Why not simply calling `gawk` explicitly instead of `awk`?
`tools/git_hook_helper.sh` could also check that `gawk` exists
Fixed in f2c363cc
@gabrielhdt Let me know when this PR will be up to date and ready for review.