Stream: Coq users

Topic: Record inside inductive types in a single expression


view this post on Zulip Daniel Hilst Selli (Dec 23 2021 at 19:36):

Is it possible to define record inside inductive type in a single expression?

In OCaml I can do something like this

type foo =
  | Bar : { name : string } -> foo
  | Tar : { age : int } -> foo

I was looking for something like

Inductive foo : Set -> Set :=
| Bar : { name : string } -> foo
| Tar : { int : age } -> foo

I can do this but by declaring records outside of foo

Record bar := { name : string }
Record tar := { int : age }

Inductive foo : Set -> Set :=
| Bar : bar -> foo
| Tar : tar -> foo

view this post on Zulip Karl Palmskog (Dec 23 2021 at 20:44):

to my knowledge there are no anonymous records in Coq. You could extend Coq with the suggested syntax (creating named records behind the user's back) using an OCaml plugin or MetaCoq

view this post on Zulip Daniel Hilst Selli (Dec 24 2021 at 14:33):

Thank you Karl!


Last updated: Sep 23 2023 at 14:01 UTC