michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/src/library
History
Leonardo de Moura faee08591f fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions 
This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not.
The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 12:12:54 -07:00
..
error_handling refactor(kernel/formatter): add formatter_factory, and simplify formatter interface 2014-07-10 18:32:00 +01:00
rewriter refactor(kernel): add heterogeneous equality back to expr 2014-02-07 10:28:10 -08:00
simplifier fix(library/simplifier): bug using congr1 theorem 2014-02-09 16:24:29 -08:00
tactic fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions 2014-07-27 12:12:54 -07:00
aliases.cpp feat(frontends/lean): search for identifiers in the stack of namespaces; reject non-atomic names as local names 2014-07-07 19:00:06 -07:00
aliases.h feat(frontends/lean): add basic pretty printer 2014-07-09 01:12:36 -07:00
bin_app.cpp feat(library/bin_app): add simpler is_bin_app predicate 2014-05-15 13:53:11 -07:00
bin_app.h feat(library/bin_app): add simpler is_bin_app predicate 2014-05-15 13:53:11 -07:00
choice.cpp fix(library/choice): style 2014-07-21 01:36:53 +01:00
choice.h feat(library): add choice expressions 2014-06-11 14:35:34 -07:00
CMakeLists.txt feat(library/head_map): a simple indexing datastructure 2014-07-08 15:08:13 -07:00
coercion.cpp refactor(kernel/instantiate): rename instantiate_params to instantiate_univ_params 2014-06-29 12:09:55 -07:00
coercion.h feat(library/coercion): add has_coercions_to function 2014-06-26 18:38:27 -07:00
decl_macros.h refactor(*): replace LEAN_THREAD_LOCAL with MK_THREAD_LOCAL_GET, the new macro uses the Boost thread_local_ptr instead of 'thread_local' directive 2014-06-07 10:18:36 -07:00
deep_copy.cpp chore(kernel/replace_fn): add syntax sugar for replace function 2014-07-19 12:53:37 +01:00
deep_copy.h refactor(kernel): move shallow copy function to library 2014-05-17 11:20:24 -07:00
explicit.cpp fix(frontends/lean/elaborator): bug when mixing implicit arguments and sections 2014-07-19 09:55:34 +01:00
explicit.h fix(frontends/lean/elaborator): bug when mixing implicit arguments and sections 2014-07-19 09:55:34 +01:00
expr_lt.cpp refactor(kernel): remove 'let'-expressions 2014-06-24 16:27:27 -07:00
expr_lt.h feat(library/expr_lt): add expr_quick_cmp functional object 2014-05-29 13:34:16 -07:00
expr_pair.h fix(library/expr_pair): typo 2014-07-15 04:11:27 +01:00
expr_pair_maps.h refactor(*): uses aliases for unordered_map and unordered_set 2013-12-18 12:30:45 -08:00
head_map.cpp feat(library/head_map): a simple indexing datastructure 2014-07-08 15:08:13 -07:00
head_map.h feat(library/head_map): a simple indexing datastructure 2014-07-08 15:08:13 -07:00
hop_match.cpp refactor(kernel): add heterogeneous equality back to expr 2014-02-07 10:28:10 -08:00
hop_match.h feat(library/simplifier): make sure the simplifier can handle meta-variables 2014-01-28 20:30:47 -08:00
hott_kernel.cpp refactor(library/unifier): move inductive datatype support to inductive_unifier_plugin 2014-07-05 11:00:35 -07:00
hott_kernel.h refactor(kernel): move standard and hott kernel instantiations to library 2014-07-05 10:31:27 -07:00
inductive_unifier_plugin.cpp fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions 2014-07-27 12:12:54 -07:00
inductive_unifier_plugin.h refactor(library/unifier): move inductive datatype support to inductive_unifier_plugin 2014-07-05 11:00:35 -07:00
io_state.cpp refactor(kernel/formatter): add formatter_factory, and simplify formatter interface 2014-07-10 18:32:00 +01:00
io_state.h refactor(kernel/formatter): add formatter_factory, and simplify formatter interface 2014-07-10 18:32:00 +01:00
io_state_stream.cpp refactor(kernel/formatter): add formatter_factory, and simplify formatter interface 2014-07-10 18:32:00 +01:00
io_state_stream.h refactor(kernel/formatter): add formatter_factory, and simplify formatter interface 2014-07-10 18:32:00 +01:00
kernel_bindings.cpp fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions 2014-07-27 12:12:54 -07:00
kernel_bindings.h refactor(kernel/formatter): add formatter_factory, and simplify formatter interface 2014-07-10 18:32:00 +01:00
kernel_serializer.cpp feat(kernel): add general purpose 'annotations', they are just a generalization of the 'let'-annotations 2014-07-25 09:33:31 -07:00
kernel_serializer.h fix(kernel): set module_idx on theorems, otherwise we are not able to import theorems that use opaque definitions 2014-06-16 16:56:11 -07:00
level_names.cpp chore(kernel/replace_fn): add syntax sugar for replace function 2014-07-19 12:53:37 +01:00
level_names.h fix(library/scope): make sure the local universe names do not conflict with universe parameter names when close a section, add declaration parameter name sanitizers 2014-06-02 15:39:57 -07:00
locals.cpp refactor(frontends/lean): use expr_struct_set when collecting locals 2014-07-14 04:12:58 +01:00
locals.h refactor(frontends/lean): use expr_struct_set when collecting locals 2014-07-14 04:12:58 +01:00
max_sharing.cpp fix(library/max_sharing): take binder annotations into account 2014-06-28 08:31:09 -07:00
max_sharing.h refactor(kernel): move max_sharing to library 2014-05-17 11:15:08 -07:00
module.cpp fix(util/rc): reference counter memory_order flags 2014-07-21 08:23:01 -07:00
module.h fix(library/module): do not store full path of imported modules 2014-06-29 10:48:57 -07:00
normalize.cpp refactor(kernel): store binder_infor in local constants 2014-06-30 11:37:46 -07:00
normalize.h feat(library): add simple normalization procedure 2014-05-20 09:40:30 -07:00
num.cpp feat(frontends/lean): parse numerals as expressions of type 'num.num' 2014-07-02 08:09:33 -07:00
num.h feat(frontends/lean): parse numerals as expressions of type 'num.num' 2014-07-02 08:09:33 -07:00
occurs.cpp refactor(kernel): move files that don't need to be in the kernel 2014-04-25 18:30:40 -07:00
occurs.h refactor(kernel): move files that don't need to be in the kernel 2014-04-25 18:30:40 -07:00
opaque_hints.cpp fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions 2014-07-27 12:12:54 -07:00
opaque_hints.h fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions 2014-07-27 12:12:54 -07:00
parser_nested_exception.h refactor(*): error messages 2014-01-13 16:54:21 -08:00
placeholder.cpp refactor(frontends/lean/elaborator): modify when tactic_hints are invoked, add the notion of strict placeholder 2014-07-14 02:53:02 +01:00
placeholder.h refactor(frontends/lean/elaborator): modify when tactic_hints are invoked, add the notion of strict placeholder 2014-07-14 02:53:02 +01:00
private.cpp feat(frontends/lean/builtin_cmds): add definition command family 2014-06-13 17:30:35 -07:00
private.h feat(frontends/lean/builtin_cmds): add definition command family 2014-06-13 17:30:35 -07:00
register_module.h feat(library): add mk_explicit/is_explicit procedures for '@'-expressions 2014-06-24 12:11:27 -07:00
resolve_macro.cpp refactor(*): rename Bool to Prop 2014-07-22 09:43:18 -07:00
resolve_macro.h feat(library/resolve_macro.cpp): add macro to encode propositional resolution proofs compactly 2014-05-15 13:53:11 -07:00
scoped_ext.cpp feat(frontends/lean): search for identifiers in the stack of namespaces; reject non-atomic names as local names 2014-07-07 19:00:06 -07:00
scoped_ext.h feat(frontends/lean): search for identifiers in the stack of namespaces; reject non-atomic names as local names 2014-07-07 19:00:06 -07:00
shared_environment.cpp chore(*): replace unique_lock with lock_guard when we do not need to use conditional variables 2014-06-07 20:55:25 -07:00
shared_environment.h perf(library/shared_environment): replace shared_mutex with simple mutex, the shared_mutex is just overhead and impacts negatively on performance tests 2014-05-27 08:34:44 -07:00
standard_kernel.cpp refactor(library/unifier): move inductive datatype support to inductive_unifier_plugin 2014-07-05 11:00:35 -07:00
standard_kernel.h refactor(kernel): move standard and hott kernel instantiations to library 2014-07-05 10:31:27 -07:00
string.cpp refactor(library/standard): rename bit to bool 2014-07-22 09:49:54 -07:00
string.h feat(frontends/lean): parse strings as expressions of type 'string.string' 2014-07-02 10:00:55 -07:00
unifier.cpp fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions 2014-07-27 12:12:54 -07:00
unifier.h fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions 2014-07-27 12:12:54 -07:00
unifier_plugin.cpp refactor(library/unifier): store the unifier_plugin in the environment 2014-07-05 10:25:58 -07:00
unifier_plugin.h refactor(library/unifier): store the unifier_plugin in the environment 2014-07-05 10:25:58 -07:00
unsolved_metavar_exception.h feat(frontends/lean): improve error message for expressions containing unsolved metavariables 2014-01-13 13:21:44 -08:00
update_declaration.cpp chore(kernel/declaration): rename declaration::get_params to declaration::get_univ_params 2014-06-02 16:20:34 -07:00
update_declaration.h feat(library): add helper functions for 'updating' declarations 2014-06-02 15:13:38 -07:00