Mario Carneiro
25aea1b723
doc: document all the tactics
2022-08-01 08:08:03 -07:00
Mario Carneiro
c952c69690
feat: add missingDocs linter
2022-07-31 18:18:21 -07:00
Sebastian Ullrich
5160cb7b0f
refactor: remove some unnecessary antiquotation kind annotations
2022-07-23 17:09:32 +02:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! ( #1354 )
2022-07-22 12:05:31 -07:00
Sebastian Ullrich
cdb855d281
feat: support all sensible modifiers on (builtin_)initialize
...
Resolves #1324
2022-07-20 22:12:20 +02:00
Leonardo de Moura
e1fc904786
feat: attributes on syntax
...
closes #1321
2022-07-18 23:37:11 -04:00
Gabriel Ebner
eba400543d
refactor: use computed fields for Name
2022-07-11 14:19:41 -07:00
Leonardo de Moura
4b543d5edd
feat: add option for disabling dsimp during simp
2022-07-10 07:57:41 -07:00
Leonardo de Moura
e4b358a01e
refactor: prepare to elaborate a[i] notation using typeclasses
2022-07-09 15:24:22 -07:00
Leonardo de Moura
2b2d4245dc
fix: extensible tactics bug
...
See comment at `expandMacros`
2022-07-05 13:20:22 -07:00
tydeu
bff560759e
feat: add missing literal TSyntax helpers
2022-07-05 13:18:58 +02:00
Gabriel Ebner
141b110ff1
feat: add more typed syntax coercions
2022-07-03 22:46:59 +02:00
Gabriel Ebner
922ef23112
fix: do not ignore syntax coercions
...
Syntax coercions do not need to be the identity. See for example
``Coe (TSyntax `ident) (TSyntax `declId)``.
2022-07-03 22:46:59 +02:00
Gabriel Ebner
ddf77a8c6d
chore: style
2022-07-03 22:46:59 +02:00
Leonardo de Moura
5e3a3a6c21
chore: remove notation a[i,h] for a[⟨i, h⟩]
2022-07-03 06:24:26 -07:00
Leonardo de Moura
a2456c3a0f
feat: add notation a[i, h] for a[⟨i, h⟩]
2022-07-02 15:50:49 -07:00
Leonardo de Moura
2ebcf29cde
chore: use a[i]! for array accesses that may panic
2022-07-02 15:12:05 -07:00
Leonardo de Moura
e8935d996b
chore: String.get?, String.getOp?, and remove String.getOp
2022-07-02 09:59:04 -07:00
Sebastian Ullrich
22475b8669
refactor: introduce common TSyntax abbreviations
2022-06-27 22:37:02 +02:00
Sebastian Ullrich
a78302243c
refactor: strengthen Syntax signatures
...
Most notable change: `Quote` is now parameterized by the target kind.
Which means that `Name` etc. could actually have different
implementations for quoting into `term` and `level`, if that need ever
arises.
2022-06-27 22:37:02 +02:00
Sebastian Ullrich
f90e4ae30c
feat: more TSyntax API & coercions
2022-06-27 22:37:02 +02:00
Sebastian Ullrich
a12cde41e1
chore: work around macro limitations
...
It would be nice if `macro` was as expressive as syntax quotations, but
right now it's not.
2022-06-27 22:37:02 +02:00
Sebastian Ullrich
e6954bb4f3
fix: quote Name.anonymous
2022-06-27 22:37:02 +02:00
Leonardo de Moura
fc25689f21
feat: add Syntax.eraseSuffix?
2022-06-27 10:30:57 -07:00
Gabriel Ebner
733f220ee3
feat: $[...]* antiquotations for sepByIndent
2022-06-24 10:59:55 +02:00
Leonardo de Moura
f6d1e48cb8
fix: constant => opaque issues
2022-06-14 17:19:54 -07:00
Leonardo de Moura
02c4e548df
feat: replace constant with opaque
2022-06-14 17:02:59 -07:00
Leonardo de Moura
041827bed5
chore: unused variables
2022-06-07 17:54:10 -07:00
Sebastian Ullrich
ae7b895f7a
refactor: unname some unused variables
2022-06-07 16:37:45 -07:00
Leonardo de Moura
c65537aea5
feat: Option is a Monad again
...
TODO: remove `OptionM` after update stage0
see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Do.20we.20still.20need.20OptionM.3F/near/279761084
2022-05-04 15:27:42 -07:00
Leonardo de Moura
02d0a89229
chore: simpStar does not make sense for dsimp
2022-04-26 11:26:54 -07:00
Leonardo de Moura
6af1da450e
feat: disable only eta for classes during TC resolution
...
closes #1123
2022-04-26 08:20:39 -07:00
Leonardo de Moura
47b379e1bc
feat: dsimp! tactic
2022-04-23 18:41:04 -07:00
Leonardo de Moura
342a26a023
feat: dsimp tactic
2022-04-23 18:05:18 -07:00
Leonardo de Moura
18832ad91c
feat: add autoUnfold to Simp.Config
...
Add macros for conveniently setting `arith` and `autoUnfold`.
2022-04-18 15:59:30 -07:00
Sebastian Ullrich
e1fbc04c3b
chore: accept unregistered syntax kinds in stage 1
2022-04-15 08:50:46 -07:00
Sebastian Ullrich
74435013f4
chore: remove now-broken workarounds
2022-04-08 15:53:58 +02:00
Leonardo de Moura
de2e2447d2
chore: style
2022-04-07 17:35:05 -07:00
Leonardo de Moura
fdd1cb5751
chore: remove workarounds for #1090
2022-04-01 11:28:17 -07:00
Leonardo de Moura
799c701f56
fix: inconsistency between syntax and kind names
...
TODO: remove staging workarounds
see #1090
2022-04-01 11:20:16 -07:00
Leonardo de Moura
68acfc7fb9
chore: prepare for #1090
2022-04-01 11:11:28 -07:00
Leonardo de Moura
3862e7867b
refactor: make String.Pos opaque
...
TODO: this refactoring exposed bugs in `FuzzyMatching` and `Lake`
closes #410
2022-03-20 10:47:13 -07:00
Leonardo de Moura
9b9ed6db68
feat: add simp_all_arith macro
2022-03-16 16:17:45 -07:00
Leonardo de Moura
ff76958959
feat: basic support for linear Nat arithmetic at simp
2022-02-26 08:58:32 -08:00
Leonardo de Moura
77dda12bc9
chore: add Simp.Config.arith option
2022-02-25 16:30:44 -08:00
Sebastian Ullrich
2c7d67d498
fix: make info of fields synthesized by structure update synthetic
2022-02-06 08:50:07 -08:00
Leonardo de Moura
12e2a79170
chore: fix codebase after removing auto pure
2022-02-03 18:08:14 -08:00
Leonardo de Moura
d4f7899591
chore: avoid code duplication setting Simp.Config
2022-01-24 18:57:31 -08:00
Leonardo de Moura
dae3489fe2
feat: remove partials from Init/Data/Array/Basic.lean
2022-01-10 16:05:33 -08:00
Leonardo de Moura
7789779020
feat: add simple default tactic for well-founded recursion
2022-01-10 14:26:08 -08:00
