Mymms Interactive Demo


Mymms is a project of computer algebra system based upon a proof assistant.

Kernel Interactive Demo

examples (to copy and paste):

A set of simple tests
A simpl matrix implementation using dependent types
A set of simple tests to illustrate overloading and coercion
The first Coq challenge
Some simple encoding (illustration of shadow typing)

Poussin Interactive Demo

examples (to copy and paste):

A set of simple tests
Illustration of automatically generated induction principles

Minima Interactive Demo

examples (to copy and paste):

A set of simple tests about mutually recursive definitions
The booleans
The numbers