To play this document inside your browser use ALT-N and ALT-P.
If you get stack overflow

errors, try to use
Google Chrome
or Chromium
with the command line option `--js-flags="--harmony-tailcalls"`.

You can
save your edits
inside your browser and
load them back
(edits are also saved when you close the window). Finally you can
download
the file for offline editing.

###
We start by loading a few libraries

#
Basics: data structures and logic

###
We open a name space to make experiments.

###
Type bool and its inhabitants:

###
Definition by pattern-matching:

###
What you see is what you get:

###
Proof by computation, using the conversion rule:

###
Case analysis justification:

###
Type nat and its inhabitants:

###
Constructors feature notations 0 and _.+1.

###
Definition by pattern-matching:

###
Definition by recurrence:

###
Definition by recurrence:

###
What is the difference between (eqn k l) and (k = l) ?

#
Inference of implicit information

###
Here is a type of polymorphic lists:

###
As such there is a verbose duplication of parameters:

###
Avoid over-specification of the theorems to be applied:

###
We can define types which pairs a data type with a specification:

###
We can use unification to infer the assumptions:

#
Oracles

###
Sorry, the demo is not available in your browser.

#
Reflection based tactics

###
Correctness relies on the assumptions on op2 and z and u:

###
This is the way the ring tactic is implemented.

#
End

###
Sorry, the end of the demo is not available in your browser.