-
Notifications
You must be signed in to change notification settings - Fork 61
Open
Description
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
Metadata
Metadata
Assignees
Labels
No labels