1 Matching Annotations
  1. Jul 2021
    1. The keyword data tells us this is an inductive definition, that is, that we are defining a new datatype with constructors

      Inductive, since multiple constructors are generalized to a type. And as seen in this example, data types can also facilitate mathematical induction.