Elias Aebi
085f51ecb9
doc: fix Markdown code-blocks
2022-09-16 05:48:44 -07:00
Leonardo de Moura
abe1f7f6f9
feat: dependency collector for the code specializer
2022-09-15 19:55:37 -07:00
Leonardo de Moura
ef636f6ec5
chore: update stage0
2022-09-15 19:02:37 -07:00
Leonardo de Moura
b77ff79133
fix: put Lean.Server.FileWorker.WidgetRequests back
2022-09-15 19:02:12 -07:00
Leonardo de Moura
c16d4fb926
chore: fix test suite
2022-09-15 18:59:51 -07:00
Leonardo de Moura
d3b0b49c43
feat: improve elabBinRelCore
...
See new test and comments at `elaBinRelCore`
2022-09-15 15:17:57 -07:00
Mario Carneiro
eac410db4e
fix: fix tests
2022-09-15 14:02:38 -07:00
Mario Carneiro
c0812d0673
chore: reorder Elab.MutualDef and Elab.Deriving.Basic
2022-09-15 14:02:38 -07:00
Mario Carneiro
b092d986dc
chore: split Lean.Data.Name and NameMap
2022-09-15 14:02:38 -07:00
Mario Carneiro
6392c5b456
chore: import reductions
2022-09-15 14:02:38 -07:00
Yuri de Wit
bbc70c4cf0
fix: fixes #1599 by adding correct indentation
2022-09-15 13:11:51 -07:00
Alex J Best
f2abe87ddf
chore: fix a typo in def name getOptionDefaulValue
...
renamed to getOptionDefaultValue
2022-09-15 11:45:45 -07:00
Leonardo de Moura
10a56bf4a1
fix: fixes #1571
...
The previous implementation was using the following heuristic
```lean
-- heuristic: use non-dependent arrows only if possible for whole group to avoid
-- noisy mix like `(α : Type) → Type → (γ : Type) → ...`.
let dependent := curNames.any fun n => hasIdent n.getId stxBody
```
The result produced by this heuristic was **not** producing an
accidental name capture, but I agree
it was confusing to have `∀ (a : True), ∃ a, a = a : Prop` instead of
`True → ∃ a, a = a : Prop` since there is no dependency.
AFAICT, all examples affected by this commit have a better output now.
cc @digma0 @kha
2022-09-15 11:16:16 -07:00
Leonardo de Moura
4f1f20bc97
refactor: ToExprM
2022-09-15 07:42:11 -07:00
Leonardo de Moura
c1b7accd12
refactor: LCNF local context
...
The previous implementation had a few issues:
- Function (and join point) declarations were being inserted into two different hashmaps.
- `borrow` information was not available for parameters.
- No proper erase functions.
2022-09-14 19:25:16 -07:00
Leonardo de Moura
9e5a818de5
fix: bug at LCNF toDecl
2022-09-14 15:23:34 -07:00
Leonardo de Moura
00e269c93c
fix: throw error at ⟨..⟩ notation if constructor is private
2022-09-14 15:02:38 -07:00
Leonardo de Moura
75f166edcc
feat: add assertNoFun test
2022-09-14 13:59:09 -07:00
Leonardo de Moura
82bba1c63b
feat: add Code.forM
2022-09-14 13:58:57 -07:00
Leonardo de Moura
ef9127487a
fix: throw error at {..} notation if constructor is private
2022-09-14 12:05:53 -07:00
Juan Pablo Romero
0742fd6fc3
docs: fix typo in SeqRight docstring
2022-09-14 10:17:15 -07:00
Gabriel Ebner
ed9b5bcb92
fix: make all syntax accessors non-panicking
2022-09-14 10:17:00 -07:00
Mario Carneiro
f6b3890dc5
feat: tail-recursive List.{mapM, foldrM}
2022-09-14 08:31:18 -07:00
Gabriel Ebner
10ff2601c5
fix: term info for inductive ctors
2022-09-14 08:26:17 -07:00
Gabriel Ebner
f1b5fa53f0
chore: use new comment syntax
2022-09-14 08:26:17 -07:00
Gabriel Ebner
b0e059318f
chore: update stage0
2022-09-14 08:26:17 -07:00
Gabriel Ebner
e04cecc496
chore: prepare for bootstrap
2022-09-14 08:26:17 -07:00
Gabriel Ebner
59abb9a332
feat: move docstring before | in ctors
2022-09-14 08:26:17 -07:00
Gabriel Ebner
00793fcdd8
chore: remove old bootstrapping hack
2022-09-14 08:26:17 -07:00
Leonardo de Moura
fccb60fb69
feat: support for [inlineIfReduce] at new compiler
2022-09-13 18:23:42 -07:00
Leonardo de Moura
e8246e026d
fix: bug at compatibleTypes
...
Many thanks to @hargoniX
2022-09-13 15:58:06 -07:00
Leonardo de Moura
8f2ab82408
fix: bug at bindCases
...
Many thanks to @hargoniX
2022-09-13 15:36:46 -07:00
Leonardo de Moura
7535c12bc5
test: add frontend meeting examples to test suite
2022-09-13 09:08:38 -07:00
Gabriel Ebner
b4af14d44a
fix: deindent docstrings with empty lines
2022-09-13 07:16:12 -07:00
Mario Carneiro
a0fcb660c5
feat: allow multiple source + no expected type
2022-09-13 07:09:08 -07:00
Mario Carneiro
adc215dab9
feat: support {s with ..}
2022-09-13 07:09:08 -07:00
Gabriel Ebner
d67546e388
chore: add test
2022-09-13 06:19:40 -07:00
Gabriel Ebner
ca28b0462c
feat: show all missing fields in structure instance
2022-09-13 06:19:40 -07:00
Gabriel Ebner
54e7d31d0f
feat: allow empty whereStructInst
2022-09-13 06:19:40 -07:00
Elias Aebi
fea65d9934
doc: fix an example in the Macro Overview
2022-09-13 03:22:38 -07:00
Mario Carneiro
3bb3efdedc
feat: allow optional type in example
2022-09-13 03:11:04 -07:00
Mario Carneiro
b4ed2f2bbb
doc: document Init.Data.Queue
2022-09-13 03:09:25 -07:00
Sebastian Ullrich
2770b9e98b
chore: inheritDoc misbehaves on built-in parsers
2022-09-13 03:08:23 -07:00
Sebastian Ullrich
a4ac7087dc
doc: some do extensions
2022-09-13 03:08:23 -07:00
Leonardo de Moura
1350a57a03
refactor: remove pure field from LCNF.LetDecl
...
We decide that in phase 3 we will assume everything is impure, and
this kind of fine-grain tracking is not worth it.
2022-09-12 19:13:43 -07:00
Leonardo de Moura
b2d6caca0a
fix: inferProjType at LCNF
2022-09-12 18:27:14 -07:00
Leonardo de Moura
a2631ce037
fix: panic when Syntax.missing
...
I got a panic error message today in VS Code because of this function.
It is weird because, as far as I can tell, this function is only used by
the `register_simp_attr` macro, and this macro was not being used in
the files I was editing.
I think the fix is resonable for a `Syntax.missing` case.
cc @gebner
2022-09-12 16:10:14 -07:00
Leonardo de Moura
506cf01d94
fix: bug at simpCasesOnCtor?
2022-09-12 16:02:19 -07:00
Leonardo de Moura
b777d411ec
feat: add useRaw parameter at constructorApp?
...
and document this API.
2022-09-12 15:56:36 -07:00
Leonardo de Moura
e08d48c591
feat: track ground let-declarations at Specialize.lean
2022-09-12 14:05:45 -07:00
