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