max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/api
History
Leonardo de Moura 9afb53fad5 feat(kernel/expr): allow metavariables to have user-facing names 
We need this feature for:
1) Defining nonlinear search patterns. Example: (?m <= ?m + 1)
2) Preprocessing recursive equations and support the pattern
refinement approach used in Agda. Example: in Agda, they accept
```
def append {A : Type} : Π (m n : nat), Vec A m -> Vec A n -> Vec A (m + n)
| m n nil            ys := ys
| m n (cons m' x xs) ys := cons x (append m' n xs ys)
```
These equations have to be refined. For example, `m` has to be
replaced with `0` (in the first equation), and `succ m'` in the
second. To implement this kind of refinement, we need to convert
the pattern variables (local constants) into metavariables during
elaboration. Then, the unassigned metavariables become local constants
again. This preprocessing step will fix some of the issues on #1594.
To completely fix #1594, we will need yet another preprocessing step
which will implement "complete transition" used in the equation
compiler before we start elim_match.cpp
2017-07-16 07:16:41 -07:00
..
CMakeLists.txt feat(api): add APIs for parsing files, commands and expressions 2015-09-08 16:44:33 -07:00
decl.cpp refactor(kernel): add reducibility_hints 2016-09-04 16:30:02 -07:00
decl.h feat(api): add lean_env API 2015-08-22 12:37:22 -07:00
env.cpp feat(kernel,library,frontends/lean,api): remove global universe levels from kernel and APIs 2017-02-08 17:41:44 -08:00
exception.cpp refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
exception.h refactor(library/exception): avoid throw_generic_exception functions 2016-09-06 12:37:56 -07:00
expr.cpp feat(kernel/expr): allow metavariables to have user-facing names 2017-07-16 07:16:41 -07:00
expr.h feat(api): add lean_decl API 2015-08-22 10:41:33 -07:00
inductive.cpp feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class 2016-09-29 17:56:35 -07:00
inductive.h chore(kernel): remove support for mutually inductive datatypes from the kernel 2016-09-10 17:39:17 -07:00
ios.cpp refactor(*): structured message objects 2016-10-13 18:49:10 -07:00
ios.h feat(api): add lean_ios API 2015-08-23 08:19:25 -07:00
lean.h feat(api): add APIs for parsing files, commands and expressions 2015-09-08 16:44:33 -07:00
lean_bool.h feat(api): expose hierarchical names in the C API 2015-08-17 17:23:10 -07:00
lean_decl.h feat(api): annotate which procedures in the API may throw high-level exceptions 2015-09-23 18:39:34 -07:00
lean_env.h feat(kernel,library,frontends/lean,api): remove global universe levels from kernel and APIs 2017-02-08 17:41:44 -08:00
lean_exception.h chore(library): remove old unifier 2016-09-19 17:18:47 -07:00
lean_expr.h feat(kernel): add let-expressions to the kernel 2016-02-29 16:40:17 -08:00
lean_inductive.h chore(kernel): remove support for mutually inductive datatypes from the kernel 2016-09-10 17:39:17 -07:00
lean_ios.h feat(api): annotate which procedures in the API may throw high-level exceptions 2015-09-23 18:39:34 -07:00
lean_macros.h feat(api): expose hierarchical names in the C API 2015-08-17 17:23:10 -07:00
lean_module.h refactor(util/lean_path): support leanpkg.path files 2017-05-01 14:11:38 -07:00
lean_name.h feat(api): annotate which procedures in the API may throw high-level exceptions 2015-09-23 18:39:34 -07:00
lean_options.h feat(api): annotate which procedures in the API may throw high-level exceptions 2015-09-23 18:39:34 -07:00
lean_parser.h feat(api): annotate which procedures in the API may throw high-level exceptions 2015-09-23 18:39:34 -07:00
lean_string.h refactor(api): uniform names 2015-08-18 11:01:46 -07:00
lean_type_checker.h refactor(kernel): simplify kernel type_checker 2016-03-18 16:28:42 -07:00
lean_univ.h feat(frontends/lean): no global universes in the frontend 2017-02-08 17:23:04 -08:00
module.cpp fix(*): gcc 7 weird uninitialized warnings 2017-05-31 18:05:03 -07:00
name.cpp feat(api): add total orders for lean_name, lean_univ and lean_expr APIs 2015-08-23 19:42:22 -07:00
name.h feat(api/name): add lean_list_name API 2015-08-21 15:04:19 -07:00
options.cpp chore(src/api/options): fix style 2015-08-18 12:43:58 -07:00
options.h feat(api): expose configuration options in the C API 2015-08-18 11:57:27 -07:00
parser.cpp refactor(frontends/lean/parser): store snapshots in a lazy async list 2017-03-27 14:00:53 -07:00
string.cpp refactor(api): uniform names 2015-08-18 11:01:46 -07:00
string.h feat(api): expose hierarchical names in the C API 2015-08-17 17:23:10 -07:00
type_checker.cpp refactor(kernel): simplify kernel type_checker 2016-03-18 16:28:42 -07:00
type_checker.h refactor(kernel): simplify kernel type_checker 2016-03-18 16:28:42 -07:00
univ.cpp feat(kernel,library,frontends/lean,api): remove global universe levels from kernel and APIs 2017-02-08 17:41:44 -08:00
univ.h feat(api/univ): add lean_list_univ API 2015-08-21 15:25:12 -07:00