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
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
Thank you Karl!
Last updated: Oct 13 2024 at 01:02 UTC