MMY MMY (Jul 24 2022 at 07:45): MMY MMY (Jul 24 2022 at 07:45):How can I represent this set union in Coq?
Domain.png
Can it be like :
Inductive Domain : Set :=
| int : nat -> Domain
| float : float -> Domain
| string : string -> Domain.
James Wood (Jul 24 2022 at 08:53):Yeah, I suppose ∪ with a dot over it represents a disjoint union, and cases of an Inductive (or Variant) give you basically that.
James Wood (Jul 24 2022 at 08:53):(This should be in a different thread, by the way.)
Last updated: Apr 20 2024 at 03:40 UTC