Wojciech Nawrocki
b1e6edefde
fix: redirect child I/O to null on Process.Stdio.null
...
And don't use errno for Win32 API errors.
2020-11-27 13:17:32 -08:00
Leonardo de Moura
5981553e11
chore: remove workaround
2020-11-27 13:15:31 -08:00
Leonardo de Moura
89298b165d
chore: update stage0
2020-11-27 13:11:11 -08:00
Leonardo de Moura
3f720d778c
fix: unnecessary unfolding
2020-11-27 13:08:18 -08:00
Leonardo de Moura
c0db9f1e0c
chore: adjust stdlib to recent changes
2020-11-27 12:26:07 -08:00
Leonardo de Moura
f2ae695e14
test: propagateExpectedType
2020-11-27 12:17:23 -08:00
Leonardo de Moura
745a41fcf0
chore: update stage0
2020-11-27 12:16:16 -08:00
Leonardo de Moura
58f1f512f1
feat: simplify heuristics at propagateExpectedType
2020-11-27 12:13:29 -08:00
Leonardo de Moura
d212a5b671
feat: add macro withoutExpectedType! <term>
2020-11-27 11:08:58 -08:00
Leonardo de Moura
09ed75f517
feat: remove restriction from propagateExpectedType
2020-11-27 09:14:26 -08:00
Leonardo de Moura
93cc8a6403
chore: fix test
...
It was working for the wrong reasons
2020-11-27 09:00:11 -08:00
Leonardo de Moura
fcc382df08
fix: improve Offset.lean
...
It did not support for assigned metavariables.
2020-11-27 08:40:43 -08:00
Leonardo de Moura
2909313475
fix: doLetArrow and doReassignArrow
...
@Kha the new tests did not work without this fix.
The `| _ =>` was being parsed as part of the `doLetArrow` and `doReassignArrow`
2020-11-26 10:29:08 -08:00
Leonardo de Moura
2c38cb56ea
test: unbundled ConstantFunction
2020-11-26 09:48:12 -08:00
Leonardo de Moura
43d98ef7e3
fix: Term/Sort parsers
...
missing `checkColGt`
2020-11-26 09:34:32 -08:00
Leonardo de Moura
ee77afafa5
doc: add typeclass.md
2020-11-26 08:42:42 -08:00
Leonardo de Moura
8898988747
fix: namespace resolution
2020-11-26 08:17:35 -08:00
Leonardo de Moura
35341e6a06
chore: update stage0
2020-11-25 18:34:06 -08:00
Leonardo de Moura
eabbb6eca0
feat: improve [defaultInstance]
...
cc @Kha
2020-11-25 18:33:06 -08:00
Leonardo de Moura
975271e1a3
feat: hide inaccessible names and add pp.inaccessibleNames
...
@Kha We will probably have to refine the heuristic for hiding the
inaccessible names, but the first version is already useful.
Here is the error message for a `_` before this commit
```
error: don't know how to synthesize placeholder
context:
x✝⁴ : List Nat
x✝³ : Nat
x✝² : x✝⁴ ≠ []
a b x✝¹ : Nat
x✝ : [a, b] ≠ []
⊢ Nat
```
After
```
error: don't know how to synthesize placeholder
a b : Nat
: [a, b] ≠ []
⊢ Nat
```
2020-11-25 17:22:09 -08:00
Leonardo de Moura
276a8b99dd
refactor: move ppGoal to Meta
...
We need `MetaM` methods such as `isProp` to improve `ppGoal`.
This commit also moves `currNamespace` and `openDecls` to
`Core.Context`. Without this change, `Meta.ppExpr` was not taking
`open` commands into account.
2020-11-25 14:17:13 -08:00
Leonardo de Moura
6f0919f08d
chore: fix places that require erewrite
2020-11-25 11:02:26 -08:00
Leonardo de Moura
c9a9dbcede
chore: update stage0
2020-11-25 11:02:26 -08:00
Leonardo de Moura
2c19eb08cb
feat: add erewrite tactic
...
This commits also change `rewrite`. It was behaving like Lean 3
`erewrite` which is too expensive.
2020-11-25 11:02:25 -08:00
Leonardo de Moura
9023e93b3e
refactor: move Array.set to Prelude
2020-11-25 11:02:25 -08:00
Sebastian Ullrich
bbe3d51c44
chore: Nix: hide some Nix warnings in lean-dev
...
/cc @javra
2020-11-25 18:37:33 +01:00
Leonardo de Moura
551d4607ae
chore: update stage0
2020-11-25 09:26:33 -08:00
Leonardo de Moura
e3fb7010f1
chore: fix tests
2020-11-25 09:25:45 -08:00
Leonardo de Moura
d6f778bec4
refactor: arbitrary without explicit arguments
...
@Kha I was tired of writing `arbitrary _` :)
There 0 places in the stdlib where the type needs to be provided.
If in the future we need to specify the type we can use
`arbitrary (α := <type>)`
2020-11-25 09:07:38 -08:00
Leonardo de Moura
5c20467600
chore: update stage0
2020-11-25 08:32:22 -08:00
Leonardo de Moura
3b75a56160
chore: prepare to make arbitrary argument implicit
2020-11-25 08:30:03 -08:00
Leonardo de Moura
6976f4501e
chore: cleanup
2020-11-25 08:19:17 -08:00
Sebastian Ullrich
de20b14366
feat: delaborate basic do
...
/cc @leodemoura
2020-11-25 16:00:56 +01:00
Sebastian Ullrich
e2ff1c2b7e
chore: update stage0
2020-11-25 12:39:26 +01:00
Sebastian Ullrich
192ee5372a
fix: Nix: update-stage0
2020-11-25 12:13:22 +01:00
Sebastian Ullrich
375e6232e0
chore: introduce doSeqItem kind
2020-11-25 12:10:49 +01:00
Sebastian Ullrich
bd7bb6f5b5
fix: do formatting
2020-11-25 11:30:24 +01:00
Sebastian Ullrich
b22e035b6f
fix: pretty print empty matchers as nomatch
...
/cc @leodemoura
2020-11-25 11:30:24 +01:00
Sebastian Ullrich
cf9a2ae6af
feat: formatter: preserve comments
2020-11-25 11:30:24 +01:00
Sebastian Ullrich
871cd105dc
feat: Syntax.updateLeading: also choose "nicer" splits
2020-11-25 11:30:24 +01:00
Sebastian Ullrich
727816e7fd
test: bring back Reformat.lean on abbreviated copy of Prelude.lean
...
/cc @leodemoura
2020-11-25 11:30:24 +01:00
Sebastian Ullrich
33c1e5ed9e
fix: formatter: ignore all but one choice node
2020-11-25 11:30:24 +01:00
Sebastian Ullrich
6126fd6388
chore: improve pretty printer traces, avoid recursion
2020-11-25 11:30:24 +01:00
Sebastian Ullrich
45a315d273
doc: Nix: seems to work fine on macOS
2020-11-25 09:48:50 +01:00
Leonardo de Moura
46dfe7b911
doc: expand tactics.md
2020-11-24 16:56:09 -08:00
Leonardo de Moura
1aeb88cee5
feat: add where example in proofs
2020-11-24 16:30:28 -08:00
Leonardo de Moura
1cb7cb3ef6
feat: add exists tactic
2020-11-24 16:17:43 -08:00
Leonardo de Moura
22629b3c66
feat: add headBetaMVarType
2020-11-24 16:17:27 -08:00
Leonardo de Moura
36eb03c601
chore: cleanup Check.lean
2020-11-24 16:13:52 -08:00
Leonardo de Moura
b72a3c69b6
fix: ambiguity at induction/cases
...
See efc3a320fe
2020-11-24 14:59:12 -08:00
