Concept
Constructor expression
Books
Journey Statuslearning Tags
[Rocq] An expression that applies a constructor to arguments to build a value of an inductive type (like S (S O) for 2, or Some 42 for an optional integer).
[Rocq] An expression that applies a constructor to arguments to build a value of an inductive type (like S (S O) for 2, or Some 42 for an optional integer).