Stream: Coq users

Topic: Record syntax questions


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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: Jan 31 2023 at 13:02 UTC