Leonardo de Moura
f056f0f2cb
refactor(library): definitional ==> constructions
2016-08-11 10:08:22 -07:00
Leonardo de Moura
f75de2e950
chore(library/definitional,frontends/lean): remove decreasing macro
2016-08-09 16:27:33 -07:00
Leonardo de Moura
efedc3f0c5
chore(library/definitional/equations): remove recursive from error messages
2016-07-22 11:14:57 -07:00
Leonardo de Moura
35888fae2c
refactor(util/list): remove coercion from T -> list<T>
2016-06-22 10:00:07 -07:00
Leonardo de Moura
a05f8719df
fix(library/definitional/equations): fix missing case
2016-06-01 19:28:48 -07:00
Leonardo de Moura
4ae7afd8c4
fix(library/definitional/equations): potential non-termination
2016-06-01 19:23:36 -07:00
Leonardo de Moura
54f68226f4
chore(frontends/lean): disable old tactic framework and blast
2016-04-25 16:22:15 -07:00
Leonardo de Moura
8dde1489f9
refactor(library/util): isolate util procedures that depend on old_type_checker
2016-03-21 13:36:08 -07:00
Leonardo de Moura
487a1e7f89
refactor(kernel): remove extension_context
...
We replaced it with abstract_type_context
2016-03-19 15:15:39 -07:00
Leonardo de Moura
e7f1f409c4
refactor(kernel): simplify kernel type_checker
...
TODO: cleanup, move justification/metavar/constraints to library
2016-03-18 16:28:42 -07:00
Leonardo de Moura
d8079aa16a
refactor(library): create copy of the kernel type_checker in library
...
Motivation: it will allow us to simplify the kernel type_checker and
make sure it implements the same API provided by type_context
2016-03-18 14:34:10 -07:00
Leonardo de Moura
3c878ecd01
feat(kernel): add let-expressions to the kernel
...
The frontend is still using the old "let-expression macros".
We will use the new let-expressions to implement the new tactic framework.
2016-02-29 16:40:17 -08:00
Leonardo de Moura
7d61f640f6
refactor(*): add abstract_type_context class
2016-02-26 14:17:34 -08:00
Leonardo de Moura
49661a043d
feat(library/definitional/equations): improve detection of infeasible cases in the definitional package
2016-02-22 14:16:24 -08:00
Leonardo de Moura
c9e9fee76a
refactor(*): remove name_generator and use simpler mk_fresh_name
2016-02-11 18:05:57 -08:00
Rob Lewis
8e428f2d3f
fix(src/library/definitional/equations.cpp): fix typo in error message
2015-09-11 08:52:53 -07:00
Leonardo de Moura
5a6a4b45c1
fix(library/definitional/equations): fixes #796
2015-08-14 14:39:23 -07:00
Floris van Doorn
fa1979c128
feat(datatypes): let the type of unit be the lowest non-Prop universe
...
The definitional package (brec_on and cases_on) now use poly_unit instead of unit
closes #698
2015-06-25 17:33:46 -07:00
Leonardo de Moura
70fc05294b
refactor(library/local_context): avoid hack in local_context
2015-06-18 15:41:00 -07:00
Leonardo de Moura
c5fb3ec6d0
fix(library/definitional/equations): fixes #541
...
This commit allows recursive applications to have less or more arguments
than the equation left-hand-side.
We add two tests
- 541a.lean recursive call with more arguments
- 542b.lean recursive call with less arguments
2015-05-10 20:37:44 -07:00
Leonardo de Moura
207e8e86da
fix(library/definitional/equations): do not clear eliminated hypotheses when invoking 'cases' tactic from definitional package
2015-05-10 11:08:02 -07:00
Leonardo de Moura
57ea660963
refactor(*): start process for eliminating of opaque definitions from the kernel
...
see issue #576
2015-05-08 16:06:04 -07:00
Leonardo de Moura
061e26157e
fix(kernel,library): make sure macros check relevant arguments when kernel is performing full type checking
2015-05-08 12:41:23 -07:00
Leonardo de Moura
4ea323a2b2
refactor(library/tactic): cleanup common pattern
2015-03-12 14:52:41 -07:00
Leonardo de Moura
4edd7b9099
fix(library/definitional/equations): allow a function to be the result of a match-with term or recursive definition
2015-03-06 15:08:52 -08:00
Leonardo de Moura
5b736a2268
feat(frontends/lean): add support for empty match-with expressions
2015-02-26 16:36:15 -08:00
Leonardo de Moura
dc2ac92846
fix(library/definitional/equations): use whnf on recursive definition arguments
...
The idea is to expose "hidden" datatypes.
2015-02-23 22:27:30 -08:00
Leonardo de Moura
27f6bfd3f0
refactor(*): add file constants.txt with all constants used by the Lean binary
2015-01-23 16:50:32 -08:00
Leonardo de Moura
e9338669dc
feat(library/definitional/equations): show implicit arguments (by default) in equations compiler error messages
2015-01-13 13:30:12 -08:00
Leonardo de Moura
e5a8c67d22
fix(library/definitional/equations): assertion violation
2015-01-13 11:57:14 -08:00
Leonardo de Moura
a3bc1b0cd5
fix(library/definitional/equations): add more equation validation to avoid obscure error message
2015-01-09 18:52:21 -08:00
Leonardo de Moura
698754b2bb
feat(library/definitional/equations): display elaborated equation lhs's when there are missing cases
2015-01-08 12:00:47 -08:00
Leonardo de Moura
5c118127ae
fix(library/definitional/equations): memory access violation
2015-01-07 17:06:41 -08:00
Leonardo de Moura
15b5344626
feat(library/definitional/equations): copy tags
2015-01-07 14:00:46 -08:00
Leonardo de Moura
760dc2162a
chore(library/definitional/equations): cleanup
2015-01-06 14:53:21 -08:00
Leonardo de Moura
a3a6697f44
feat(library/definitional/equations): mutually recursive functions for mutually recursive datatypes
2015-01-06 14:07:17 -08:00
Leonardo de Moura
322cdb8a98
feat(library/definitional/equations): add 'equations_result' macro used to wrap multiple functions being defined by recursive equations
...
This is only useful when compiling "mutually recursive" functions.
2015-01-05 19:09:20 -08:00
Leonardo de Moura
3325d791de
fix(library/definitional/equations): bug in recursive application elimination
2015-01-05 17:17:14 -08:00
Leonardo de Moura
eedc31f7e9
fix(library/definitional/equations): bug in "complete" transition
2015-01-05 16:27:29 -08:00
Leonardo de Moura
3889b60152
feat(library/definitional/equations): allow inductive datatype parameters in recursive equations
2015-01-05 15:56:28 -08:00
Leonardo de Moura
6eba4b4ac1
chore(library/definitional/equations): cleanup
2015-01-05 13:57:13 -08:00
Leonardo de Moura
b46c377aa2
feat(library/definitional/equations): add "complete" transition for overlapping patterns
2015-01-05 11:49:27 -08:00
Leonardo de Moura
fdef3e5407
feat(library/definitional/equations): add support for reflexive datatypes in the definitional package
2015-01-05 11:13:35 -08:00
Leonardo de Moura
5e228d92d2
fix(library/definitional/equations): missing case
2015-01-04 20:49:53 -08:00
Leonardo de Moura
faf78ce3e6
feat(library/definitional/equations): brec_on compilation
2015-01-04 17:45:13 -08:00
Leonardo de Moura
926c140e17
fix(library/definitional/equations): fix clang compilation problems
2015-01-04 10:18:19 -08:00
Leonardo de Moura
bdfa919098
feat(library/definitional/equations): add brec_on based compilation
2015-01-03 22:23:37 -08:00
Leonardo de Moura
376126241e
fix(library/definitional/equations): typo and bug
2015-01-03 15:29:34 -08:00
Leonardo de Moura
21a9cd58a3
fix(library/definitional/equations): bug when compiling in proof relevant kernels
2015-01-02 23:17:33 -08:00
Leonardo de Moura
7f7d318b22
feat(library/definitional/equations): add dependent pattern matching compilation
2015-01-02 22:06:40 -08:00
