doc(examples/lean): add theorem sent by Jeremy Avigad

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): allow user to import several theories using a single import

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/elaborator): hack for fixing a bug due to pairs/projs, this is temporary fix until we build a new elaborator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(builtin): define list, cons, nil and prove basic theorems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(builtin/kernel): rename refute to by_contradiction

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(builtin/num): define fact and exp

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(builtin/num): bug in the factorial definition

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/type_checker): caching bug

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
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>