Changeset 2542


Ignore:
Timestamp:
Dec 7, 2012, 11:13:00 AM (7 years ago)
Author:
mulligan
Message:

Trying an Agda port of the polymorphic variants implementation to see how tedious it is. Major stumbling block at the moment is the lack of coercions. Suggested solution is to use type classes, but this doesn't seem very nice either.

Location:
Papers/polymorphic-variants-2012
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/polymorphic-variants-2012/polymorphic-variants.tex

    r2526 r2542  
    758758Here, \texttt{mk\_DeqSet} is the constructor of the \texttt{DeqSet} record.
    759759By convention in Matita, for a record type name \texttt{Foo}, there exists a constructor for that record type name \texttt{mk\_Foo}.
    760 We pass the constructor function three arguments: the type that possess a decidable equality, in this case \texttt{tag\_}
     760We pass the constructor function three arguments: the type that possess a decidable equality---in this case \texttt{tag\_}---the equality function itself, and a proof that propositional equality and decidable equality co-incide for this type.
     761In this case, the final argument to \texttt{mk\_DeqSet} is posed as a proof obligation (marked by `\texttt{?}'), which is closed via Matita's tactic interface below the definition.
    761762
    762763\bibliography{polymorphic-variants}
Note: See TracChangeset for help on using the changeset viewer.