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

coq.env.add-indt not preserving implicit arguments #574

Open
FissoreD opened this issue Jan 23, 2024 · 0 comments
Open

coq.env.add-indt not preserving implicit arguments #574

FissoreD opened this issue Jan 23, 2024 · 0 comments

Comments

@FissoreD
Copy link
Collaborator

The problem:
the API coq.env.add-indt does not preserve the implicitness of arguments while adding the new indt.

Code example:

Elpi Command add_indt.
Elpi Accumulate  lp:{{
  main [indt-decl X] :- 
    coq.env.add-indt X _. % simply adding the indt in elpi
}}.

Definition X (b : bool) := Type.

Elpi add_indt Record NoWheels {i : nat} := {
  (* the first and the third arguments of no_wheels are implicit! *)
  no_wheels (u : unit) {b : bool} : X b
}.

Expected results:
About no_wheels should say that Arguments no_wheels {i}%nat_scope n u {b}%bool_scope
however, we have, Arguments no_wheels i%nat_scope record u b%bool_scope

Test:
Check (no_wheels 0 _ tt true). should fail
Check (no_wheels _ tt). should succeed

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

1 participant