1 Matching Annotations
  1. Jul 2021
  2. plfa.github.io plfa.github.io
    Naturals: Natural numbers
    1
    1. bbarker 18 Jul 2021
      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.

      Programming Functional Logic Agda
    Visit annotations in context

    Tags

    Annotators

    URL

    plfa.github.io/Naturals/