Skip to content

Philosophy [The Programming "Package"]

gmalecha edited this page Oct 9, 2012 · 1 revision

The Programming "package" is new in version 0.2. It is motivated by the desire to leverage Coq's expressive type system to build a powerful "programming" language (rather than a completely expressive proof language). The easiest way to see this is in the use of type classes in a way slightly opposed to the ideas expressed in "Philosophy [Use of Type Classes]".

Clone this wiki locally