feat(builtin/kernel): prove false_elim without using case

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(builtin/proof_irrel): prove proof irrelevance

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(builtin/kernel): use standard definition for 'or' and 'and'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
doc(builtin): Diaconescu’s theorem

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean): help msg

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(builtin): simulate binary encoding

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/elaborator): temporary fix for bug reported by Jeremy

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(examples/lean): small version of algebraic hierarchy (proof of concept)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/elaborator): add hack for experimenting with algebraic hierarchy

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(examples/lean): opaque pairs

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
doc(examples/wf): use 'have' construct in wf example

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(builtin): simpler encoding of sum types

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(builtin): quotient types

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(src/builtin): precompiled .olean binary

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/script_state): deadlock, add example exposing the problem

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(README): remove coverall badge, it is a link for the official repository

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(README): layout

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontents/lean/parser_cmds):
Print the type of variables introduced by definition, hypothesis (variable) or proof.
fix(kernel/level): bug reported by Floris

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser_cmds): add 'print definition' command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>