Floris van Doorn
3d0d0947d6
various cleanup changes in library
...
some of the changes are backported from the hott3 library
pi_pathover and pi_pathover' are interchanged (same for variants and for sigma)
various definitions received explicit arguments: pinverse and eq_equiv_homotopy and ***.sigma_char
eq_of_fn_eq_fn is renamed to inj
in definitions about higher loop spaces and homotopy groups, the natural number arguments are now consistently before the type arguments
2018-09-10 17:59:11 +02:00
Floris van Doorn
27cde0aeae
feat(hott): rename ppi_gen to ppi
2017-07-21 15:53:34 +01:00
Floris van Doorn
a02ea6b751
Unfold macros using the full typechecker in normalize.
...
Fix #7 . The problem (as I understand it) was that macros were expanded using a typechecker which didn't unfold (semireducible) definitions, which led to the macros not being unfolded correctly.
Many many many thanks to @gebner!
2017-07-20 12:09:39 +01:00
Leonardo de Moura
4d4a0c7c53
chore(tests/lean/run/num_norm1): remove test for broken tactic
2016-12-30 13:59:58 -08:00
Leonardo de Moura
a086fb3348
chore(tests/lean/interactive): remove broken old tests
2016-12-02 16:55:23 -08:00
Floris van Doorn
e87a27cb4b
fix(hott/init/path): reorder arguments of whisker_right
2016-12-02 16:55:23 -08:00
Floris van Doorn
70a5f98747
fix(tests): fix crash1
2016-09-22 18:47:47 -04:00
Leonardo de Moura
a5fb28ca78
chore(frontends/lean,tests): fix tests and style
2016-07-09 10:29:34 -07:00
Floris van Doorn
e4071639f1
fix(builtin_cmds): metavar_args should be false by default
2016-07-09 10:21:17 -07:00
Floris van Doorn
fb81bcaeee
fix(tests): fix tests after changes is the HoTT library
2016-07-09 10:20:22 -07:00
Sebastian Ullrich
e9a6a532ab
fixup! also allow shadowing non-constructor definitions
2016-07-09 10:19:23 -07:00
Sebastian Ullrich
d7789fa58a
feat(frontends/lean): support variables shadowing in patterns
2016-07-09 10:19:23 -07:00
Sebastian Ullrich
87c5ba9f52
Revert "fix(library/definitional/equations): add more equation validation to avoid obscure error message"
...
This reverts commit a3bc1b0cd5
2016-07-09 10:19:23 -07:00
Sebastian Ullrich
54844e2325
feat(frontends/lean): add parent classes to local context in struct definitions
...
Fixes #1066
2016-07-05 19:39:57 -07:00
Sebastian Ullrich
c73b2860d5
fix(frontends/lean): uniform handling of declaration compound names
...
* allow compound names in `namespace` and `structure`
* adjust error messages
2016-06-02 18:07:03 -07:00
Leonardo de Moura
b58eac5013
chore(tests/lean/extra): fix test
2016-06-02 11:28:00 -07:00
Sebastian Ullrich
273753f3fc
chore(tests): mass-update for pp.binder_types false
2016-06-02 11:28:00 -07:00
Sebastian Ullrich
f2200fab65
feat(frontends/lean/pp): add option to hide binder types
2016-06-02 11:28:00 -07:00
Leonardo de Moura
933b5863cd
fix(tests/lean/770): adjust test output
...
Pull request #1037 changed error message but did not correct test output.
2016-04-11 09:50:46 -07:00
Daniel Selsam
eeee7d51cf
chore(kernel/error_msgs): show inferred type when function expected
2016-04-11 09:47:14 -07:00
Floris van Doorn
f983724cf6
feat(pointed): merge pointed2 into pointed
...
We move the basic notions of pointed types into init.pointed, to avoid cycles in the import graph. Also adds pointed versions of pi and sigma, with corresponding notation
2016-04-11 09:45:59 -07:00
Floris van Doorn
dc37ec954d
refactor(hott): rename apdo to apd
2016-04-11 09:45:59 -07:00
Floris van Doorn
05b59aecf8
refactor(hott): rename apd to apdt
2016-04-11 09:45:59 -07:00
Floris van Doorn
ea775092bb
fix(tests): use have instead of assert
2016-03-06 11:25:14 -05:00
Floris van Doorn
5cacebcf86
feat(hott): replace assert by have and merge namespace equiv.ops into equiv
...
The coercion A ≃ B -> (A -> B) is now in namespace equiv. The notation ⁻¹ for symmetry of equivalences is not supported anymore. Use ⁻¹ᵉ
2016-03-03 10:13:21 -08:00
Leonardo de Moura
d84a20d68b
remove(frontends/lean/server): FINDG command
2016-03-03 10:12:24 -08:00
Jeremy Avigad
4050892889
refactor(library/*): rename 'compose' to 'comp'
2016-03-02 22:48:05 -05:00
Daniel Selsam
c23528b5d8
feat(library/blast/blast): use defeq_simplifier to normalize
2016-03-01 13:44:33 -08:00
Leonardo de Moura
fbe5188480
refactor(frontends/lean): remove 'by+' and 'begin+' tokens
2016-02-29 13:45:43 -08:00
Leonardo de Moura
b41c65f549
feat(frontends/lean): remove '[visible]' annotation, remove 'is_visible' tracking
2016-02-29 12:31:23 -08:00
Leonardo de Moura
101cf1ec4c
feat(frontends/lean): remove difference between 'have' and 'assert'
2016-02-29 11:28:20 -08:00
Leonardo de Moura
7d61f640f6
refactor(*): add abstract_type_context class
2016-02-26 14:17:34 -08:00
Leonardo de Moura
5a4dd3f237
feat(library/reducible): remove [quasireducible] annotation
2016-02-25 17:42:44 -08:00
Leonardo de Moura
1924b2884c
refactor(library/tactic): remove 'append' and 'interleave' tacticals
...
Preparation for major refactoring in the tactic framework.
2016-02-24 16:02:16 -08:00
Leonardo de Moura
2a294bcc17
fix(frontends/lean/elaborator): fixes #996
2016-02-22 17:03:14 -08:00
Leonardo de Moura
96f391dda2
feat(library/definitional/projection,frontends/lean/structure_cmd): creating inductive predicates using structure command
2016-02-22 16:09:44 -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
Jeremy Avigad
0f81c2e65b
fix(tests/lean/noncomp_theory,simlifier_light): fix tests
2016-02-22 11:25:23 -08:00
Floris van Doorn
b2181497fd
fix(tests): fix delta_issue2
2016-02-22 11:15:38 -08:00
Floris van Doorn
4e2cc66061
style(*): rename is_hprop/is_hset to is_prop/is_set
2016-02-22 11:15:38 -08:00
Daniel Selsam
d521063dfb
feat(library/defeq_simplifier): new simplifier that uses only definitional equalities
2016-02-22 11:01:36 -08:00
Leonardo de Moura
20f70035dd
fix(frontends/lean/util): fixes #1007
2016-02-22 10:54:55 -08:00
Daniel Selsam
bb4b8da582
feat(library/unification_hint): basic handling of user-supplied unification hints
2016-02-12 11:48:51 -08:00
Leonardo de Moura
c9e9fee76a
refactor(*): remove name_generator and use simpler mk_fresh_name
2016-02-11 18:05:57 -08:00
Leonardo de Moura
f67181baf3
chore(*): remove support for Lua
2016-02-11 17:17:55 -08:00
Daniel Selsam
f06cdff2a1
fix(library/blast/simplifier/ceqv): fix error in is_permutation
2016-02-07 14:06:28 -08:00
Leonardo de Moura
30d6853ffd
refactor(hott,tests): make sure HoTT library and tests still work if we introduce checkpoints in have-expressions
2016-02-04 16:58:32 -08:00
Leonardo de Moura
a08bc408c8
fix(frontends/lean/structure_cmd): fixes #967
2016-02-04 16:15:18 -08:00
Leonardo de Moura
31cc0ebb6a
fix(frontends/lean/structure_cmd): fixes #968
2016-02-04 15:45:38 -08:00
Leonardo de Moura
496c84dac6
fix(frontends/lean/elaborator): fixes #982
2016-02-04 15:14:30 -08:00
