Stream: Coq users

Topic: Record inside inductive types in a single expression

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

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

Daniel Hilst Selli (Dec 24 2021 at 14:33):

Thank you Karl!

Last updated: Oct 13 2024 at 01:02 UTC