Leonardo de Moura
61ecf018e9
feat(frontends/lean,library/tactic): add easy tactic parsing support for at ... and with ...
2015-12-17 12:18:32 -08:00
Leonardo de Moura
c824a0e050
chore(library,hott): enforce naming conventions
2015-12-17 11:36:58 -08:00
Sebastian Ullrich
2185ee7e95
feat(library/tactic): make let tactic transparent, introduce new opaque note tactic
...
The new let tactic is semantically equivalent to let terms, while `note`
preserves its old opaque behavior.
2015-12-14 10:14:02 -08:00
Leonardo de Moura
95fba3dba6
chore(library/constants): sort constant decls
2015-12-13 21:39:45 -08:00
Leonardo de Moura
193a9d8cde
refactor(library/norm_num): avoid manual constant name initialization
...
@rlewis1988 We group all Lean constants used in the C++ code at
src/library/constants.txt
Jeremy and Floris check this file before renaming constants in the
library. So, they can quickly decide whether C++ code will be affected
or not.
We also have a python script for initializing the C++ name objects.
To use the script:
- go to src/library
- execute
python ../../script/gen_constants_cpp.py constants.txt
It will create the boring initialization and finalization code, and
declare a procedure get_<id>_name() for each constant in the file constants.txt.
I also move the norm_num1.lean to the set of unit tests that are
executed whenever we push a commit to the main branch.
I found an assertion violation at line 606. Could you take a look?
Best,
Leo
2015-12-13 21:38:59 -08:00
Leonardo de Moura
85379b7706
feat(library/blast/actions/simple_actions): make sure contradiction action works even if classical logic support is not enabled
...
not (not (not a)) -> not a
2015-12-07 09:30:14 -08:00
Leonardo de Moura
80725cc416
fix(library): references to algebra in the source code
2015-12-05 23:50:26 -08:00
Daniel Selsam
08e0fc796b
feat(library/blast/actions): by_contradiction action
2015-12-04 20:19:05 -08:00
Leonardo de Moura
2682fe9525
feat(library/blast/blast): force 'ne' to be always transparent
2015-12-04 18:24:36 -08:00
Leonardo de Moura
00e34683f2
feat(library/app_builder): (try to) address not-issue and other reducibility annotation related issues in the app_builder
2015-12-04 16:03:06 -08:00
Daniel Selsam
2bf9989bd9
refactor(library/blast/unit): simplify module
2015-12-04 08:30:03 -08:00
Leonardo de Moura
83b9769225
fix(library/blast): init_classical_flag
...
The procedure get_namespaces does not return the set of opened
namespaces. I added a comment there to clarify that.
2015-12-04 08:13:19 -08:00
Daniel Selsam
0dfac6d07e
feat(library/blast): classical flag
2015-12-04 07:53:05 -08:00
Leonardo de Moura
3de9a89d93
feat(library/blast/congruence_closure): congruence_closure basics
2015-11-17 18:45:22 -08:00
Leonardo de Moura
16bcd2f522
feat(congr_lemma_manager): add congruence lemma for equivalence relation over iff/eq
2015-11-17 18:45:22 -08:00
Daniel Selsam
5e8068b2b2
feat(library/blast/simplifier): draft of fusion
2015-11-16 09:13:07 -08:00
Daniel Selsam
f72da014d4
feat(library/blast/fusion): refactor
2015-11-16 09:13:07 -08:00
Leonardo de Moura
4d68e2a520
feat(library,hott): add eq.mpr and eq.mp lemmas
2015-11-14 15:40:47 -08:00
Leonardo de Moura
f19fcf255a
chore(library/constants.cpp): regenerate automatically generated file
2015-11-08 14:05:03 -08:00
Daniel Selsam
8e5e8e6540
feat(library/blast/simplifier): basic infrastructure
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
5a48a2cebe
feat(library/app_builder): add mk_sorry method
2015-11-08 14:05:02 -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
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
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
b777375469
fix(frontends/lean/parser): decimals
2015-11-08 14:04:56 -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
8ee214f133
checkpoint: new numeral encoding
2015-11-08 14:04:55 -08:00
Leonardo de Moura
5d8d226640
fix(frontends/lean/parser): add support for decimals
...
Decimal numbers are notation for rationals.
If rat.of_num is not available, then an error is generated.
closes #793
2015-08-11 18:44:48 -07:00
Leonardo de Moura
e74c6eef3d
feat(library/simplifier): add 'simp.funext' and 'simp.propext' options
2015-07-21 18:23:10 -07:00
Leonardo de Moura
5581b735f4
feat(library/constants.txt): add poly_unit and poly_unit.star
2015-06-25 17:36:34 -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
1cbace9df6
feat(library/tactic/congruence_tactic): add congruence lemma generator
...
The generated congruence theorems ignore arguments that are subsingleton types.
2015-06-05 22:00:10 -07:00
Leonardo de Moura
dce86b3a84
feat(library/init/logic): add 'eq.drec' (in standard Lean) with a signature very similar to eq.rec in the HoTT library
2015-06-03 17:29:26 -07:00
Leonardo de Moura
d95c064a29
feat(library/simplifier/ceqv): add to_ceqv procedure
2015-05-27 16:35:56 -07:00
Leonardo de Moura
b1ece388a6
feat(frontends/lean,library/tactic/induction_tactic): improve induction tactic notation, expand induction tactic implementation
2015-05-18 09:25:07 -07:00
Leonardo de Moura
84faef5d5d
feat(library/tactic/rewrite_tactic): rewrite tactic with 'iff' lemmas
2015-05-14 18:27:13 -07:00
Leonardo de Moura
065a1f7501
feat(library/tactic): add 'induction' tactic skeleton
2015-05-12 20:21:25 -07:00
Leonardo de Moura
aff9257c72
feat(frontends/lean): allow → to be used in calc proofs
...
see issue #586
2015-05-07 12:28:47 -07:00
Leonardo de Moura
415ca2b93f
feat(library/tactic): add 'congruence' tactic
...
It is the f_equal described at issue #500 .
2015-05-02 12:58:46 -07:00
Leonardo de Moura
9ba8b284a1
fix(library/tactic/apply_tactic): add eapply, and fix issue #361
2015-05-01 15:08:00 -07:00
Leonardo de Moura
2d9c950144
feat(library/tactic/constructor_tactic): allow 'constructor' tactic without index
...
see issue #500
2015-04-30 21:15:07 -07:00
Leonardo de Moura
9c8a63caec
feat(library/tactic): add 'contradiction' tactic
...
see issue #500
Remark: this tactic also applies no_confusion to take care of a contradiction
2015-04-30 13:47:40 -07:00
Leonardo de Moura
3233008039
feat(library/tactic): allow user to name generalized term in the 'generalize' tactic
...
closes #421
2015-04-30 11:57:40 -07:00
Leonardo de Moura
d2c7b5c319
feat(library/tactic): add 'let' tactic
...
closes #555
2015-04-28 17:24:43 -07:00
Leonardo de Moura
ca8943f45b
feat(library,hott): remove rapply tactic
2015-04-27 15:06:16 -07:00
Leonardo de Moura
9d01868361
feat(frontends/lean): use rewrite tactic to implement unfold (it has a unfold step)
...
closes #502
2015-04-24 17:23:12 -07:00
Leonardo de Moura
2613e7c444
fix(frontends/lean): bug when handling identifiers in tactics
...
This bug was reported by Jeremy in the Lean Google group:
https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/lean-discuss/ZKJ8WPPEVJA/n05x6rPRzvMJ
2015-04-22 16:03:22 -07:00
Leonardo de Moura
6f6d106a10
feat(library/tactic): add "check_expr" tactic
...
closes #486
2015-04-19 19:00:05 -07:00
Leonardo de Moura
2bc13f6bfd
feat(library/tactic/exact): enforce goal type during elaboration when executing 'exact' tactic
...
Remark: this was the behavior of the 'sexact' tactic.
This commit also adds the 'rexact' (relaxed exact) tactic which does not
enforce the goal type.
closes #495
2015-04-06 13:23:38 -07:00
