Li-yao (Jan 05 2021 at 19:29): Li-yao (Jan 05 2021 at 19:29):Apparently type inference for record fields doesn't take into account the known type of the record:
Record R (n : nat) :=
{ fd : 3 = n + 1 }.
(* Doesn't remember that n = 2 *)
Fail Definition r : R 2 :=
{| fd := eq_refl |}.
(* Explicit annotation to give unification a hint *)
Definition r : R 2 :=
{| fd := eq_refl : 3 = 2 + 1 |}.
(1) Is there some dedicated syntax to (re)specify those indices without losing record notation?
(2) In records we can use := to introduce definitions derived from other fields, but those become global definitions, which means that two records in the same module can't use := with the same name. Any way to make it not generate a definition?
Paolo Giarrusso (Jan 05 2021 at 19:33):(1) does Program Definition do better, with its bidirectional typechecking?
(2) what about wrapping the records in Module Export foo. ... End foo. to avoid the "same module" part?
Li-yao (Jan 05 2021 at 19:56):Both of those work! Thanks :)
Maybe there's also some way to not make these extra fields show up in Search?
Gaëtan Gilbert (Jan 05 2021 at 21:00):instead of program you can use bidi hints Arguments Build_R _ & _. (as many _ before the & as there are params)
(https://coq.github.io/doc/master/refman/language/extensions/arguments-command.html?highlight=bidi#bidirectionality-hints)
Paolo Giarrusso (Jan 05 2021 at 21:26):Search has a blacklist, but it's name based (and I'm not sure how well it works — I get blacklisted program obligations often enough).
Last updated: Oct 13 2024 at 01:02 UTC