How is it possible to define abstract types in Agda. We use typedecl in Isabelle to do so.
More precisely, I would like the agda counterpart of the below code in Isabelle:
typedecl A
Thanks
How is it possible to define abstract types in Agda. We use typedecl in Isabelle to do so.
More precisely, I would like the agda counterpart of the below code in Isabelle:
typedecl A
Thanks
Copyright © 2021 Jogjafile Inc.
You could use parametrized modules. Let's have a look at an example: we start by introducing a record
Nats
packing aSet
together with operations on it.We can then define a module parametrized by such a structure. Addition and multiplication can be defined in terms of primitive recursion, zero and successor.
Finally we can provide instances of
Nats
. Here I reuse the natural numbers as defined in the standard library but one could use binary numbers for instance.Passing this instance to the module, gives us the corresponding add / mult operations: