tydeu
38a0d1e373
chore: update Lake
2023-01-28 18:29:00 +01:00
github-actions[bot]
57b9d25d5e
doc: update changelog
2023-01-19 09:10:27 +00:00
github-actions[bot]
6e5ba6b9e5
doc: update changelog
2023-01-09 23:09:06 +00:00
github-actions[bot]
d3c852a3b1
doc: update changelog
2022-12-21 21:00:58 +00:00
github-actions[bot]
75f8ebdd19
doc: update changelog
2022-11-24 03:08:45 +00:00
github-actions[bot]
140d10819d
doc: update changelog
2022-11-11 08:13:31 +00:00
github-actions[bot]
d7636694a8
doc: update changelog
2022-11-08 16:29:53 +00:00
github-actions[bot]
cf35416f5b
doc: update changelog
2022-11-07 19:01:40 +00:00
github-actions[bot]
3fdbfa2ed4
doc: update changelog
2022-11-07 18:11:29 +00:00
github-actions[bot]
ac23228c6e
update changelog
2022-10-28 19:26:19 +00:00
github-actions[bot]
24d91094f3
update changelog
2022-10-23 19:12:23 +00:00
Sebastian Ullrich
bc1a2dcaf2
chore: update RELEASES.md
2022-10-14 16:18:27 +02:00
Gabriel Ebner
1de142a20b
chore: update release notes
2022-10-11 17:24:35 -07:00
Leonardo de Moura
c7fad1815c
chore: update release notes
2022-09-30 09:31:03 -07:00
Leonardo de Moura
91e27668ae
doc: release notes
2022-09-25 07:06:50 -07:00
Leonardo de Moura
578adcd7f0
chore: release date for m5
2022-08-07 09:51:35 -07:00
tydeu
e470dad36c
chore: update Lake
2022-08-06 10:20:54 +02:00
Leonardo de Moura
f0272d9309
feat: multiple namespaces in mutual declarations
2022-08-04 19:18:49 -07:00
Leonardo de Moura
2e37582f31
feat: allow users to install their own deriving hanlders for builtin classes
2022-08-02 08:29:24 -07:00
Leonardo de Moura
99413a18ff
feat: add congr tactic
2022-08-01 18:44:07 -07:00
Leonardo de Moura
0156b59ef1
chore: enforce naming convention
2022-08-01 09:58:11 -07:00
Leonardo de Moura
c76fa06816
chore: update release notes
2022-07-31 18:25:48 -07:00
Leonardo de Moura
37af11ae20
fix: unused match-syntax alternatives are silently ignored
...
closes #1371
2022-07-31 06:00:08 -07:00
Leonardo de Moura
a63cb24a38
feat: structure field auto-completion
2022-07-30 14:40:21 -07:00
Leonardo de Moura
83ee9b1a57
feat: auto-completion for dotted identifier notation
2022-07-30 10:21:04 -07:00
Leonardo de Moura
3dfa895bf0
feat: OfNat instance postprocessor
...
Closes #1389
2022-07-30 08:35:45 -07:00
Leonardo de Moura
3e4a805b5b
chore: typo
2022-07-28 20:12:20 -07:00
Leonardo de Moura
012cb13f51
feat: add [elabAsElim] elaboration strategy
2022-07-28 20:08:29 -07:00
Leonardo de Moura
163fe62ac7
chore: update release notes
2022-07-28 15:18:40 -07:00
Sebastian Ullrich
a2ccf8f122
feat: accept keywords as constructor names
2022-07-28 12:46:28 -07:00
Leonardo de Moura
49ce4408df
feat: validate parametric local instances
...
Closes #1373
2022-07-27 16:09:56 -07:00
Leonardo de Moura
642cf0bc6d
feat: add option pp.showLetValues
...
closes #1345
2022-07-26 17:53:34 -07:00
Leonardo de Moura
d6f0880d11
feat: add option warningAsError
2022-07-26 05:57:54 -07:00
Leonardo de Moura
b3b2a07ed0
feat: support dotted notation and named arguments in patterns
2022-07-25 18:19:32 -07:00
Leonardo de Moura
40936d52bd
chore: improve [deprecated] example at release notes
2022-07-25 12:32:15 -07:00
Leonardo de Moura
f83846b481
chose: update release notes
2022-07-25 12:28:23 -07:00
Leonardo de Moura
8335a82aed
refactor: improve MVarId method discoverability
...
See issue #1346
2022-07-24 21:36:33 -07:00
Leonardo de Moura
b6e9d58537
feat: add [deprecated] attribute
2022-07-24 18:06:03 -07:00
Leonardo de Moura
a62949c49b
refactor: add type LevelMVarId (and abbreviation LMarId)
...
Motivation: make sure we do not mixup metavariable ids for
expression and universe level.
cc @bollu
2022-07-24 17:21:45 -07:00
Leonardo de Moura
5e877b115b
feat: improve calc tactic
...
> Heather suggested changing the calc tactic (not the term) such that if
the final RHS does not defeq match the goal RHS, it returns a final
inequality as a subgoal.
Closes #1342
2022-07-24 14:30:15 -07:00
Sebastian Ullrich
e5891850a7
doc: update RELEASES.md
2022-07-23 17:09:32 +02:00
Leonardo de Moura
af1e670270
chore: fix typo
2022-07-11 15:46:54 -07:00
Gabriel Ebner
86ccba8c87
chore: update release notes
2022-07-11 12:26:53 -07:00
Gabriel Ebner
b1eb022027
feat: computed fields
2022-07-11 12:26:53 -07:00
Leonardo de Moura
fd0e9e1c52
chore: fix typo
2022-07-10 10:15:29 -07:00
Leonardo de Moura
351fc6ea04
chore: update release notes
2022-07-10 09:43:25 -07:00
Leonardo de Moura
49951b87b9
chore: update release notes
2022-07-09 17:02:15 -07:00
Leonardo de Moura
58619291e9
feat: better qualified name support in recursive definitions
2022-07-07 20:15:25 -07:00
tydeu
6e4bca57c8
chore: update Lake
2022-07-05 17:27:41 -07:00
Leonardo de Moura
8f83999202
chore: update release notes
2022-07-03 06:26:47 -07:00
