Leonardo de Moura
6f01a7339a
refactor(library/blast): move simple search strategy to separate module
2015-11-10 11:44:18 -08:00
Leonardo de Moura
6ac2bf9c6c
refactor(library/blast): add choice_point object
2015-11-10 11:28:59 -08:00
Leonardo de Moura
b76cdb1c68
refactor(library/blast): move blast options to separate module
2015-11-10 11:03:54 -08:00
Leonardo de Moura
f1c2a88e17
feat(library/blast): add proof_expr thin layer for creating proof terms at blast
2015-11-10 10:50:58 -08:00
Leonardo de Moura
5304f62f54
feat(library/blast/hypothesis): track proof depth in hypotheses
2015-11-10 09:54:28 -08:00
Leonardo de Moura
409ad18f9b
refactor(library/blast/state): cleanup state interface
2015-11-10 09:20:44 -08:00
Daniel Selsam
fc5dba4cd1
fix(library/simplifier/simp_rule_set): use lists instead of vectors
2015-11-10 08:58:46 -08:00
Leonardo de Moura
b59dd2305c
refactor(library/blast): rename state::get ==> state::get_hypothesis_decl
2015-11-09 14:52:21 -08:00
Leonardo de Moura
fb7a47cf2b
refactor(library/blast): avoid auxiliary local when creating hypothesis for intros
2015-11-09 14:40:39 -08:00
Leonardo de Moura
a14bb86148
feat(library/blast/state): add mk_lambda/mk_pi for abstracting hrefs
2015-11-09 14:20:19 -08:00
Leonardo de Moura
973a5c4812
feat(library/blast): improve blast type_context push/pop operations
2015-11-09 13:36:49 -08:00
Leonardo de Moura
9c364b410e
refactor(library/blast): hypothesis m_depth ==> m_dep_depth
2015-11-09 13:29:07 -08:00
Leonardo de Moura
9a557958f4
refactor(library/blast): merge state and branch classes
...
We will keep only one active branch in blast.
All other branches are implicit.
2015-11-09 13:24:30 -08:00
Leonardo de Moura
9bdf3a0d33
refactor(library/blast): we should reuse uref/mref/href in idxs
...
Motivation: avoid nasty bugs when caching results
2015-11-09 12:41:52 -08:00
Leonardo de Moura
d952a1d299
refactor(library/blast/expr): remove unnecessary complexity
2015-11-09 12:27:33 -08:00
Leonardo de Moura
c5117785a8
feat(library/blast): add intros action
2015-11-08 19:18:40 -08:00
Leonardo de Moura
78f1679b03
feat(library/blast): add basic assumption action
2015-11-08 18:16:34 -08:00
Leonardo de Moura
6340b1ae5b
feat(library/blast): very basic search procedure and iterative deepening
2015-11-08 17:57:37 -08:00
Leonardo de Moura
1d39b6d5d4
feat(util/rb_map): add erase_min
2015-11-08 17:29:30 -08:00
Leonardo de Moura
c1392e60be
feat(util/rb_tree): add double_cmp
2015-11-08 17:10:49 -08:00
Leonardo de Moura
8308e87a6c
feat(library/blast/blast): initialize local instances at type_context objects
2015-11-08 15:20:05 -08:00
Leonardo de Moura
39019b6873
refactor(library/blast/simplifier): use app_builder mk_congr, mk_congr_arg and mk_congr_fun
2015-11-08 14:05:03 -08:00
Leonardo de Moura
1374f8cba1
fix(library/blast/simplifier): compilation warnings
2015-11-08 14:05:03 -08:00
Leonardo de Moura
b8857b078b
feat(library/blast): add get_app_builder to blast API
2015-11-08 14:05:03 -08:00
Leonardo de Moura
1d1f043192
refactor(library/app_builder): throw exception instead of returning none_expr
2015-11-08 14:05:03 -08:00
Daniel Selsam
0061d595d0
feat(library/blast/simplifier): use generated congruence lemmas
2015-11-08 14:05:03 -08:00
Daniel Selsam
b2368ba81b
style(library/blast/simplifier): whitespace
2015-11-08 14:05:03 -08:00
Daniel Selsam
f1d5cc5d5b
test(library/blast/simplifier): add asserts
2015-11-08 14:05:03 -08:00
Leonardo de Moura
afc7a2af84
feat(library/blast): expose mk_congr_lemma_for_simp and get_fun_info
2015-11-08 14:05:03 -08:00
Leonardo de Moura
f74e8288bd
refactor(library/congr_lemma_manager): API
2015-11-08 14:05:03 -08:00
Leonardo de Moura
f19fcf255a
chore(library/constants.cpp): regenerate automatically generated file
2015-11-08 14:05:03 -08:00
Daniel Selsam
f3caeb77cd
style(library/blast/simplifier): whitespace
2015-11-08 14:05:03 -08:00
Daniel Selsam
6c2c82f47c
feat(library/blast/simplifier): conditional rewriting
2015-11-08 14:05:03 -08:00
Daniel Selsam
d4e410162b
feat(library/blast/simplifier): expand macros
2015-11-08 14:05:02 -08:00
Daniel Selsam
b727d5810a
feat(library/blast/simplifier): rewrite with tmp locals
2015-11-08 14:05:02 -08:00
Daniel Selsam
3f331a261a
fix(library/blast/simplifier): stack of caches for local context
2015-11-08 14:05:02 -08:00
Daniel Selsam
b81aa35221
feat(library/blast/simplifier): more informative tracing
2015-11-08 14:05:02 -08:00
Daniel Selsam
0ad41173bb
fix(library/blast/simplifier): caches for each relation
2015-11-08 14:05:02 -08:00
Daniel Selsam
a304f6a9df
fix(library/blast/simplifier): loop rewrite rules
2015-11-08 14:05:02 -08:00
Daniel Selsam
a73e4e30a3
feat(library/blast/simplifier): use new blast_tmp_type_context constructor
2015-11-08 14:05:02 -08:00
Daniel Selsam
8e5e8e6540
feat(library/blast/simplifier): basic infrastructure
2015-11-08 14:05:02 -08:00
Leonardo de Moura
78a9116a23
chore(library/congr_lemma_manager): fix style
2015-11-08 14:05:02 -08:00
Leonardo de Moura
77c0866599
feat(library/congr_lemma_manager): fallback to simple congruence theorem if needed
2015-11-08 14:05:02 -08:00
Leonardo de Moura
0eb0a679e8
feat(library/congr_lemma_manager): add support for complex lemmas
2015-11-08 14:05:02 -08:00
Leonardo de Moura
ba477a0e98
feat(library/congr_lemma_manager): handle simple congruence lemmas
2015-11-08 14:05:02 -08:00
Leonardo de Moura
3dc8f72c32
feat(frontends/lean/builtin_cmds): display congr lemma arg mask
2015-11-08 14:05:02 -08:00
Leonardo de Moura
df94864809
fix(library/congr_lemma_manager): use abstract_local
2015-11-08 14:05:02 -08:00
Leonardo de Moura
8a7321714a
feat(library/congr_lemma_manager): add mk_congr_simp that takes the number of expected arguments
...
Use sorry to be able to test first part
2015-11-08 14:05:02 -08:00
Leonardo de Moura
5a48a2cebe
feat(library/app_builder): add mk_sorry method
2015-11-08 14:05:02 -08:00
Leonardo de Moura
c16423194c
feat(library/fun_info_manager): add method for getting information about function prefix
2015-11-08 14:05:02 -08:00
Leonardo de Moura
559c5a26a3
fix(library/congr_lemma_manager): take resulting type into account when computing congruence lemma
2015-11-08 14:05:02 -08:00
Leonardo de Moura
b89b4cb5f0
fix(library/fun_info_manager): bug tracking dependecies
2015-11-08 14:05:02 -08:00
Leonardo de Moura
76032eea90
feat(kernel/expr): change dummy expression used in default constructor
2015-11-08 14:05:02 -08:00
Leonardo de Moura
7d588636a1
feat(library/fun_info_manager): collect additional information
2015-11-08 14:05:02 -08:00
Leonardo de Moura
9b34526030
feat(frontends/lean): add #congr debugging command
2015-11-08 14:05:02 -08:00
Leonardo de Moura
22dcf6825e
feat(library/congr_lemma_manager): add congr_lemma_manager skeleton and compute type of congruence lemma
...
proof is still missing
2015-11-08 14:05:02 -08:00
Leonardo de Moura
01bde866d6
feat(library/util): add auxiliary recognizers
2015-11-08 14:05:01 -08:00
Leonardo de Moura
2d04156959
fix(library/app_builder): bug in eq_drec
2015-11-08 14:05:01 -08:00
Leonardo de Moura
34d5882b9a
refactor(library/util): rename old is_eq_rec
2015-11-08 14:05:01 -08:00
Leonardo de Moura
2482c49729
test(frontends/lean): add #replace command for debugging purposes
2015-11-08 14:05:01 -08:00
Leonardo de Moura
6519e570f3
feat(library/fun_info_manager): safer "replace" function
2015-11-08 14:05:01 -08:00
Leonardo de Moura
78b1d4279b
fix(library/blast/state): compilation problems in debug mode
2015-11-08 14:05:01 -08:00
Leonardo de Moura
7e7919950d
fix(library/type_context): compilation warning
2015-11-08 14:05:01 -08:00
Leonardo de Moura
8d9d84f33c
refactor(library/blast): we don't require maximally shared terms anymore in blast
...
This commit also removes the blast::mk_* expr and level functions.
They were just noops.
I kept only mk_uref, mk_href and mk_mref
2015-11-08 14:05:01 -08:00
Leonardo de Moura
45c02cb65c
feat(library/blast/blast): add extra constructor
2015-11-08 14:05:01 -08:00
Leonardo de Moura
980eb95e0c
fix(library/type_context,library/blast/blast): blast uses multiple type_context objects, this commit makes sure all of them use the same local name generator
2015-11-08 14:05:01 -08:00
Leonardo de Moura
749d468440
feat(library): add fun_info_manager
2015-11-08 14:05:01 -08:00
Leonardo de Moura
e23523bb02
feat(library/type_context): add mk_subsingleton_instance
2015-11-08 14:05:01 -08:00
Daniel Selsam
a104b478f3
feat(library/type_context): make expand_macro public
2015-11-08 14:05:01 -08:00
Leonardo de Moura
f84f024b92
refactor(library/app_builder): change app_builder constructor
2015-11-08 14:05:01 -08:00
Leonardo de Moura
98b79373cc
feat(library/blast/blast): add blast::internalize
2015-11-08 14:05:01 -08:00
Leonardo de Moura
43efc11f36
feat(library/blast/blast): automatically clear tmp_type_context at recycling time
2015-11-08 14:05:01 -08:00
Leonardo de Moura
3517a3dfa9
feat(library/blast): add blast_tmp_type_context
2015-11-08 14:05:01 -08:00
Leonardo de Moura
b2c9f2f6c5
feat(library/type_context): document our approach for managing meta-variables in type_context
2015-11-08 14:05:01 -08:00
Leonardo de Moura
aa697206e8
refactor(library/type_context): rename set_context to set_local_instances
2015-11-08 14:05:01 -08:00
Leonardo de Moura
fb7efa9337
feat(library/type_context): new tmp local_constant policy
2015-11-08 14:05:01 -08:00
Leonardo de Moura
333ba83087
feat(library/type_context): add mk_tmp_local that allows us to specify the pretty printing name
...
We also modify the type inference procedure to preserve the binder names.
2015-11-08 14:05:01 -08:00
Leonardo de Moura
01259a2d1c
feat(library/app_builder): add helper functions for creating eq.rec applications
2015-11-08 14:05:01 -08:00
Leonardo de Moura
5b71025b07
fix(library/blast/blast): temporary type_context for blast must handle external meta-variables.
2015-11-08 14:05:01 -08:00
Leonardo de Moura
d1fa547335
feat(frontends/lean/builtin_cmds): change mask notation at #app_builder command
2015-11-08 14:05:01 -08:00
Leonardo de Moura
f21102a725
feat(frontends/lean): add test commands for new app_builder features
2015-11-08 14:05:01 -08:00
Leonardo de Moura
1c2c2a6077
feat(library/app_builder): mk_app with mask
2015-11-08 14:05:01 -08:00
Leonardo de Moura
8e0a3eec3f
chore(library/relation_manager): fix bogus style warnings
2015-11-08 14:05:01 -08:00
Leonardo de Moura
0f631889b7
feat(library/app_builder): add helper methods for creating binary relations, and refl/symm/trans proofs
2015-11-08 14:05:00 -08:00
Leonardo de Moura
b5c40e30ef
feat(library/app_builder): add set_context
2015-11-08 14:05:00 -08:00
Leonardo de Moura
137ec27059
feat(library/app_builder): add constructor for app_builder that may take subclasses of tmp_type_context
...
We need this feature because blast has its own version of tmp_type_context.
2015-11-08 14:05:00 -08:00
Leonardo de Moura
ee0974650a
feat(library/app_builder): new app_builder on top of type_context
...
The new version is more robust, and invokes type class resolution if needed.
2015-11-08 14:05:00 -08:00
Leonardo de Moura
87ec7383dd
fix(library/tmp_type_context): initialization
2015-11-08 14:05:00 -08:00
Leonardo de Moura
a26ea2a249
feat(frontends/lean/builtin_cmds): add command for testing app_builder
2015-11-08 14:05:00 -08:00
Leonardo de Moura
3804281919
refactor(library/app_builder): remove app_builder Lua API
2015-11-08 14:05:00 -08:00
Leonardo de Moura
f8916ed411
feat(library/blast/blast): create tmp_type_context that is compatible with blast
2015-11-08 14:05:00 -08:00
Leonardo de Moura
e01f2ec6a5
feat(library/tmp_type_context): add temporary type_context
2015-11-08 14:05:00 -08:00
Leonardo de Moura
18d9272f22
refactor(library/type_context): revise get_assignment
...
It is safer to return optional.
2015-11-08 14:05:00 -08:00
Leonardo de Moura
3bc5084bf6
refactor(library/simplifier): disable file
...
We will eventually delete it.
It will be subsumed by blast.
2015-11-08 14:05:00 -08:00
Leonardo de Moura
27904787fe
refactor(library/type_inference): rename type_inference module to type_context
2015-11-08 14:05:00 -08:00
Daniel Selsam
ffc168d63a
fix(frontends/lean/elaborator): visit_app partial
2015-11-08 14:05:00 -08:00
Leonardo de Moura
ab940a2001
feat(frontends/lean/elaborator): add support for partial explicit in the elaborator
2015-11-08 14:05:00 -08:00
Daniel Selsam
6b06a19294
chore(frontends/lean): remove whitespace
2015-11-08 14:05:00 -08:00
Daniel Selsam
fa58d7c71e
feat(frontends/lean): basic support for partial explicit
2015-11-08 14:05:00 -08:00
Daniel Selsam
946e00f71a
feat(library/explicit): support partial explicit
2015-11-08 14:05:00 -08:00
Leonardo de Moura
1d670e3193
feat(frontends/lean): support for '@@' -- the partial explicit operator
2015-11-08 14:05:00 -08:00
Leonardo de Moura
914f3b4e34
chore(library/blast/blast): fix style
2015-11-08 14:05:00 -08:00
Leonardo de Moura
0e4f97792e
feat(library/blast): add blast::scope_debug auxiliary class for testing blast related procedures
2015-11-08 14:05:00 -08:00
Leonardo de Moura
fd917effad
feat(library/blast): use new type_inference module in blast
2015-11-08 14:05:00 -08:00
Leonardo de Moura
52eb787288
refactor(library/type_inference): move (non-temporary) class.* options to type_inference module
2015-11-08 14:05:00 -08:00
Leonardo de Moura
56c15f4fb5
refactor(library/type_inference): move new type class resolution procedure to genere type_inference
2015-11-08 14:05:00 -08:00
Leonardo de Moura
4c573380b2
feat(library/class): add auxiliary methods
2015-11-08 14:05:00 -08:00
Leonardo de Moura
c361fc1f6f
fix(frontends/lean/parser): method for parsing decimals
...
"division" has been renamed to "div"
2015-11-08 14:04:59 -08:00
Leonardo de Moura
6fa4691eb4
feat(library/type_inference): improve process_assignment
2015-11-08 14:04:59 -08:00
Leonardo de Moura
ab1937d46e
feat(library/class_instance_resolution): add new (temporary) option class.force_new to force the new type class resolution procedure in HoTT mode
2015-11-08 14:04:59 -08:00
Floris van Doorn
46dba4ee5e
refactor(category): move some files to subfolders, and create file with basic functors
2015-11-08 14:04:59 -08:00
Floris van Doorn
f2d07ca23c
feat(category): various small changes in category theory
2015-11-08 14:04:59 -08:00
Floris van Doorn
de1c47eda9
feat(categories): add exponential laws for categories
...
also give nicer rules to construct equalities between (pre)categories
2015-11-08 14:04:59 -08:00
Floris van Doorn
21723a82b6
fix(lean-syntax): add some more syntax for categories
2015-11-08 14:04:59 -08:00
Floris van Doorn
a358813182
feat(lean-syntax): fix and extend syntax highlighting
2015-11-08 14:04:58 -08:00
Floris van Doorn
3f0d8c0a8c
feat(category.adjoint): prove more about functors
2015-11-08 14:04:58 -08:00
Floris van Doorn
c7fd29f854
feat(category): start with the introduction rule for equivalences
2015-11-08 14:04:58 -08:00
Leonardo de Moura
410c9aef79
chore(library/type_inference): fix style
2015-11-08 14:04:58 -08:00
Leonardo de Moura
6465b16951
fix(library/class_instance_resolution): memory initialization bug in new type class resolution procedure
2015-11-08 14:04:58 -08:00
Leonardo de Moura
95348bc90b
fix(library/class_instance_resolution): uninitialized variables
2015-11-08 14:04:58 -08:00
Leonardo de Moura
50186e2db3
feat(library/class_instance_resolution): add old type class resolution procedure back to be able to compile HoTT library
2015-11-08 14:04:58 -08:00
Leonardo de Moura
885393f4de
feat(library/type_inference): check types when assigning meta-variables
2015-11-08 14:04:58 -08:00
Leonardo de Moura
766fdd415a
feat(library/type_inference): postpone "nontrivial" universe unification constraints
2015-11-08 14:04:58 -08:00
Leonardo de Moura
0bf069f016
feat(library/class_instance_resolution): more liberal type class resolution procedure
...
This modification is needed for the group_theory folder
2015-11-08 14:04:58 -08:00
Leonardo de Moura
21501ccfa4
fix(library/type_inference): temporary hack for solving universe unification problems
...
We need a better solution. It turns out the universe constraints are not
as simple as we expected.
2015-11-08 14:04:58 -08:00
Leonardo de Moura
5f43b9b183
feat(library/class_instance_resolution): recursively invoke type class resolution when parameters are instances
2015-11-08 14:04:58 -08:00
Leonardo de Moura
6acf7afa16
fix(library/type_inference): bug when using apply_beta
2015-11-08 14:04:58 -08:00
Leonardo de Moura
8d8e43abfd
fix(library/class_instance_resolution): transitive instances in the new type class resolution procedure
2015-11-08 14:04:58 -08:00
Leonardo de Moura
a1d200e1c6
feat(library/class_instance_resolution): add support for nested type
...
class resolution
2015-11-08 14:04:58 -08:00
Leonardo de Moura
e9b92adf29
feat(library/type_inference,library/class_instance_resolution): add on_is_def_eq_failure "event handler"
2015-11-08 14:04:57 -08:00
Leonardo de Moura
21bd30d51a
fix(library/class_instance_resolution): bug in mk_choice_point
2015-11-08 14:04:57 -08:00
Leonardo de Moura
0446c43ebf
refactor(library/class_instance_resolution): use new generic type_inference module to implement type class resolution
2015-11-08 14:04:57 -08:00
Leonardo de Moura
73543f1279
fix(library/norm_num): use new type-class resolution procedure at norm_num
2015-11-08 14:04:57 -08:00
Leonardo de Moura
f371182a6c
feat(library/type_inference): generic and cheap type inference, unification, whnf
2015-11-08 14:04:57 -08:00
Leonardo de Moura
a7655b7d43
feat(library/class_instance_resolution): reset internal indices
2015-11-08 14:04:57 -08:00
Leonardo de Moura
1f01e5480d
fix(library/class_instance_resolution): remove reset_cache_and_ctx used for debugging purposes
2015-11-08 14:04:57 -08:00
Leonardo de Moura
2edccf007b
fix(library/class_instance_resolution): make sure that terms synthesized by type class resolution have override the ones synthesized by solving unification constraints.
2015-11-08 14:04:57 -08:00
Leonardo de Moura
b71a68c606
fix(frontends/lean/elaborator): visit_prenum was creating unnecessary universe metavariable
...
This was creating problems for the new type class resolution procedure
since visit_prenum was also not creating any constraint that enforced
the universe level of A to be equal to the superfluous universe level.
2015-11-08 14:04:57 -08:00
Leonardo de Moura
4787cf179e
fix(library/class_instance_resolution): skip (instance) meta-variables that have been assigned by solving unification constraints
2015-11-08 14:04:57 -08:00
Leonardo de Moura
eb2236f036
feat(library/class_instance_resolution): bug in mk_choice
2015-11-08 14:04:57 -08:00
Leonardo de Moura
97407eb178
fix(library/class_instance_resolution): add hack for mk_subsingleton_instance API
...
The comment in the source code explains why the hack is needed
2015-11-08 14:04:57 -08:00
Leonardo de Moura
1b92a8333e
fix(library/class_instance_resolution): better is_def_eq for universe levels at new type class resolution procedure
2015-11-08 14:04:57 -08:00
Leonardo de Moura
6b4a891adb
fix(library/class_instance_resolution): bug when creating auxiliary meta-variables at try_instance
2015-11-08 14:04:57 -08:00
Leonardo de Moura
919d55b799
fix(library/class_instance_resolution): position information in the type class trace
2015-11-08 14:04:57 -08:00
Leonardo de Moura
088b0fb795
fix(library/class_instance_resolution): relax has_expr_metavar test at mk_choice
2015-11-08 14:04:57 -08:00
Leonardo de Moura
5f90ff0f07
fix(library/class_instance_resolution): incorrect assertion
2015-11-08 14:04:57 -08:00
Leonardo de Moura
443aca6280
chore(library/class_instance_resolution,library/init_module): fix style
2015-11-08 14:04:57 -08:00
Leonardo de Moura
abcfe0d805
feat(library/class_instance_resolution): add support for attribute [multiple-instances] in the new type class resolution procedure
2015-11-08 14:04:57 -08:00
Leonardo de Moura
2c177d595c
fix(library/class_instance_resolution): bug in cache validation
2015-11-08 14:04:57 -08:00
Leonardo de Moura
343ede3fbe
fix(library/class_instance_resolution): trace option for new type class resolution procedure
2015-11-08 14:04:57 -08:00
Leonardo de Moura
98943f7832
fix(library/class_instance_resolution): initialization bug and ignore universe metavariables not instantiated by unifier
2015-11-08 14:04:57 -08:00
Leonardo de Moura
6a36bffe4b
fix(library/class_instance_resolution): bugs in new type class resolution procedure
2015-11-08 14:04:57 -08:00
Leonardo de Moura
bf17440f31
feat(library/class_instance_resolution): throw exception is maximum depth is reached
2015-11-08 14:04:57 -08:00
Leonardo de Moura
f5819fab60
feat(library/class_instance_resolution): new type class resolution procedure
2015-11-08 14:04:57 -08:00
Leonardo de Moura
c69bbd4eb7
chore(library/norm_num,library/tactic/norm_num_tactic): fix style
2015-11-08 14:04:57 -08:00
Leonardo de Moura
bda0b038b0
fix(library/norm_num): include 'constants.h' instead of 'constants.cpp'
...
By including 'constants.cpp' we get compilation errors in some
platforms (e.g., 'g_one has been defined in multiple files...')
The module constants(.h/cpp) does not expose global variables such as g_one.
We have to use the procedures get_one_name() instead.
2015-11-08 14:04:56 -08:00
Rob Lewis
ce1cbcc205
feat(library/norm_num): give better error message when norm_num fails
2015-11-08 14:04:56 -08:00
Rob Lewis
eb0b688da8
style(library/norm_num): remove debug code
2015-11-08 14:04:56 -08:00
Rob Lewis
958add9ef8
feat(library/norm_num): fix numeral normalization to work on new numeral structure; add support for multiplication
2015-11-08 14:04:56 -08:00
Leonardo de Moura
f4ce2bcbfe
fix(library/CMakeLists): build
2015-11-08 14:04:56 -08:00
Leonardo de Moura
3b6eae1907
feat(library): start new type class resolution procedure
2015-11-08 14:04:56 -08:00
Leonardo de Moura
ee924e4842
fix(library/blast/infer_type): typos
2015-11-08 14:04:56 -08:00
Leonardo de Moura
4f394bd979
feat(library/meng_paulson): minor improvement
2015-11-08 14:04:56 -08:00
Leonardo de Moura
5b6b8257d8
chore(library/meng_paulson): fix style
2015-11-08 14:04:56 -08:00
Leonardo de Moura
b7e79dea29
fix(frontends/lean/parser): bug in parse_double
2015-11-08 14:04:56 -08:00
Leonardo de Moura
ee347772d7
feat(library/meng_paulson): ignore class and class-instances when computing set of relevant theorems
2015-11-08 14:04:56 -08:00
Leonardo de Moura
023ec1ba76
feat(library): add Meng&Paulson heuristic for selecting theorems
2015-11-08 14:04:56 -08:00
Leonardo de Moura
d64b410bbd
feat(library): add declaration statistics
2015-11-08 14:04:56 -08:00
Leonardo de Moura
6df31d3406
refactor(library/data/nat/basic): mark some theorems as protected to avoid overloading
2015-11-08 14:04:56 -08:00
Leonardo de Moura
2b3af47fcf
feat(frontends/lean/pp): pretty print "num numerals" too
...
This is an useful for "eval" demos
2015-11-08 14:04:56 -08:00
Leonardo de Moura
7838ed386d
refactor(frontends/lean/pp,library/init/reserved_notation): pretty print "nat numerals" nicely even when namespace nat is not open
2015-11-08 14:04:56 -08:00
Leonardo de Moura
cd144993c0
chore(frontends/lean/prenum,library/tactic/rewrite_tactic): fix style
2015-11-08 14:04:56 -08:00
Leonardo de Moura
b777375469
fix(frontends/lean/parser): decimals
2015-11-08 14:04:56 -08:00
Leonardo de Moura
38c433dbec
fix(frontends/lean/util): bug when parsing priorities
2015-11-08 14:04:55 -08:00
Leonardo de Moura
1f5d950b46
feat(frontends/lean/inductive_cmd): add options for disabling the automatic generation of auxiliary recursors
2015-11-08 14:04:55 -08:00
Leonardo de Moura
d1e111fd6c
fix(hott,frontends/lean,library,library/tactic): make sure we can still compile the HoTT library
2015-11-08 14:04:55 -08:00
Leonardo de Moura
26eb6fa849
feat(*): new numeral encoding
2015-11-08 14:04:55 -08:00
Leonardo de Moura
8ee214f133
checkpoint: new numeral encoding
2015-11-08 14:04:55 -08:00
Leonardo de Moura
8f18532a39
fix(emacs/lean-syntax): syntax highlight for [coercions]
2015-11-08 14:04:55 -08:00
Leonardo de Moura
744d1cba3d
feat(library,hott,frontends/lean): avoid keywords with hyphen
2015-11-08 14:04:54 -08:00
Leonardo de Moura
a618bd7d6c
refactor(library): use type classes for encoding all arithmetic operations
...
Before this commit we were using overloading for concrete structures and
type classes for abstract ones.
This is the first of series of commits that implement this modification
2015-11-08 14:04:54 -08:00
Soonho Kong
a25b43f1e8
feat: do not generate leanstatic.a in EMSCRIPTEN build
2015-11-03 18:22:05 -05:00
Sebastian Ullrich
7c047def97
feat(frontends/lean/parser): recognize padded Exprs terminators
2015-10-13 09:52:35 -07:00
Sebastian Ullrich
dbfebd5409
feat(frontends/lean/scanner): add more checks to read_quoted_symbol
2015-10-13 09:52:35 -07:00
Sebastian Ullrich
6c34718cbc
chore(library,frontends/lean): remove option pp.extra_spaces
...
Obsoleted by improved pretty printer spacing
2015-10-13 09:52:35 -07:00
Leonardo de Moura
c5d614d4d9
feat(library/norm_num): store the local context
2015-10-08 13:22:37 -07:00
Leonardo de Moura
ce6e1c9694
feat(library/class_instance_synth): add helper mk_class_instance procedure
2015-10-08 13:10:41 -07:00
Leonardo de Moura
2c7d245bbe
fix(library/blast/blast): bug when translating goal metavariables into
...
blast mref's
2015-10-08 13:10:41 -07:00
Leonardo de Moura
5d3ed8a634
fix(library/blast/hypothesis): hypotheses are initially inactive
2015-10-08 13:10:41 -07:00
Leonardo de Moura
e4f0f6a9b4
feat(library): numeral normalization skeleton
2015-10-08 12:49:12 -07:00
Leonardo de Moura
3bb09e9959
fix(library/blast): typos
2015-10-06 08:35:24 -07:00
Leonardo de Moura
c626e2e3c6
refactor(library/blast): divide hypotheses in: assumption, active and todo
...
The sets active and todo are disjoint.
A metavariable declaration can only depend on assumptions.
2015-10-04 21:59:37 -07:00
Leonardo de Moura
44881552b4
refactor(library/blast): refactor hypothesis object: merge m_value and m_justification fields
2015-10-04 21:27:39 -07:00
Leonardo de Moura
7b883cae8f
feat(library/blast): simplify metavar_decl
2015-10-04 18:24:21 -07:00
Leonardo de Moura
4ab14e709e
feat(library/blast): finish is_def_eq/unifier for blast tactic
2015-10-03 18:19:05 -07:00
Leonardo de Moura
a446c54b87
fix(tests/kernel/max_sharing): max_sharing on OSX
2015-10-03 12:12:21 -07:00
Leonardo de Moura
cd48114c47
fix(library/blast/infer_type): type of mref's
2015-10-02 15:53:22 -07:00
Leonardo de Moura
0a3fbda050
feat(library/blast): convert universe metavariables into uref's
2015-10-02 15:50:41 -07:00
Leonardo de Moura
442cbff578
feat(library/blast): add blast tactic is_def_eq procedure (aka unification)
...
We still have to implement subst_mref, assign_mref, and occurs check.
2015-10-02 15:21:28 -07:00
Leonardo de Moura
d324d54d21
fix(kernel/expr): add global expressions storing Prop and Type.{1} to
...
hash-consing cache when max-sharing is enabled
2015-10-02 15:04:10 -07:00
