Leonardo de Moura
7aa028ed2f
chore: update stage0
2021-02-04 18:03:39 -08:00
Leonardo de Moura
aae8a35150
feat: add ForIn type class
2021-02-04 17:59:44 -08:00
Leonardo de Moura
b9f5e2a3ad
chore: fix test output
2021-02-04 17:43:56 -08:00
Leonardo de Moura
92d97f4cc5
chore: update stage0
2021-02-04 17:39:33 -08:00
Leonardo de Moura
e415cfa632
chore: increase synthInstance.maxHeartbeats default
2021-02-04 17:36:12 -08:00
Leonardo de Moura
73e718c5eb
chore: update stage0
2021-02-04 17:22:43 -08:00
Leonardo de Moura
d956f0ae9f
feat: use destructTuple to compile for in notation instead of pattern matchin
2021-02-04 17:17:51 -08:00
Leonardo de Moura
c747230e28
refactor: move isMonad? to AppBuilder.lean
2021-02-04 17:17:51 -08:00
Leonardo de Moura
e2028e64ff
feat: add option maxUniverseOffset
...
Universe level offsets are supposed to be small numbers in practice.
2021-02-04 17:17:51 -08:00
Leonardo de Moura
d494756d00
fix: inline loop
2021-02-04 17:17:51 -08:00
Leonardo de Moura
768f2642bd
chore: document why alternative Stream design does not work
2021-02-04 17:17:51 -08:00
Sebastian Ullrich
bdf7b15a41
feat: basic unexpanders for Exists & Sigma
...
A bit brittle and not quite complete, but probably good enough in practice
2021-02-04 11:04:37 +01:00
Leonardo de Moura
545ed50f83
chore: update stage0
2021-02-03 15:11:25 -08:00
Leonardo de Moura
dae0132439
fix: save/restore state at elabTypeWithAutoBoundImplicit
2021-02-03 15:04:18 -08:00
Leonardo de Moura
e63111b39a
fix: fixes #302
...
TODO: investigage error message duplication
2021-02-03 15:04:18 -08:00
Leonardo de Moura
1a15b0183b
chore: occursCheck semantics was confusing
2021-02-03 15:04:18 -08:00
Leonardo de Moura
d1efcab6f5
perf: improve occursCheck
2021-02-03 15:04:18 -08:00
Leonardo de Moura
2510c0cb4a
chore: cleanup
2021-02-03 15:04:18 -08:00
Leonardo de Moura
33e71116a5
chore: add missing deriving Inhabited
2021-02-03 15:04:18 -08:00
Sebastian Ullrich
e6ab402c42
chore: update stage0
2021-02-03 15:25:41 +01:00
Sebastian Ullrich
bd5225aa09
fix: make forwardMessages tail-recursive
...
Just something I noticed while failing to debug an (apparently) unrelated issue hanging Emacs
2021-02-03 15:24:12 +01:00
Leonardo de Moura
f780efa476
chore: fix test
2021-02-02 14:01:53 -08:00
Leonardo de Moura
f4c9f7e163
chore: remove id_delta (aka idDelta)
...
It is a leftover from Lean 3.
2021-02-02 13:59:37 -08:00
Leonardo de Moura
bda39b9a72
feat: extend set of valid characters that can occur in an auto bound implicit local name suffix
2021-02-02 10:29:29 -08:00
Leonardo de Moura
729047b5a2
feat: auto bound implicit at constructors
...
@Kha This commit adds auto bound implicits to constructors.
I was excited until I tried to define the `Bigstep` type again without
`autoBoundImplicitLocal`, and found small typos.
Example, I had
```
| ifTrue : eval σ₁ b = true → Bigstep (c₁, σ₁) σ₂ t → Bigstep (cond b c₁ c₂, σ₁) σ₂ (t₁ + 1)
```
where `t₁` should be `t`, but the declaration was accepted. I am
wondering whether Isabelle performs some kind of sanity checking,
and/or enforces rules such as: auto-bound implicits may only be
introduced by hypotheses.
Note that this is not an issue for definitions, because the body of
the definition will probably not type check when we have this kind of
typo in the header.
Anyway, I am putting the experiment in this branch for now.
That being said, the `Bigstep` declaration is way nicer with
`autoBoundImplicitLocal`s.
Another option is to add a new option `ctorAutoBoundImplicitLocal`
that is false by default, and activates auto implicit locals for
constructors when set to true.
2021-02-02 10:18:21 -08:00
Leonardo de Moura
61c922b518
chore: add comment
2021-02-02 10:10:32 -08:00
Sebastian Ullrich
f80147e264
doc: update dev setup editor instructions
2021-02-02 17:30:51 +01:00
Sebastian Ullrich
4772fb5849
feat: delaborator: use ∀ if prop
2021-02-02 13:54:34 +01:00
Sebastian Ullrich
b83875301a
chore: move test without output
...
/cc @leodemoura
2021-02-02 13:37:56 +01:00
Sebastian Ullrich
dd6c291788
fix: relax eager mvar instantiation during constructor elaboration
...
@leodemoura: Could you double-check?
2021-02-02 13:19:15 +01:00
Leonardo de Moura
b6ba346f2a
test: add cases alternative @ test
2021-02-01 18:24:50 -08:00
Leonardo de Moura
fba719ff02
chore: adjust WF.lean
2021-02-01 18:08:48 -08:00
Leonardo de Moura
a7d2edd333
chore: update stage0
2021-02-01 18:04:28 -08:00
Leonardo de Moura
2888e49785
feat: @ modifier at induction and cases tactic alternatives
2021-02-01 18:03:19 -08:00
Leonardo de Moura
c1dce595a5
feat: add option useNamesForExplicitOnly to introN
2021-02-01 17:35:48 -08:00
Leonardo de Moura
e583b3bdc0
feat: allow @ modifier at inductionAlt
2021-02-01 17:13:51 -08:00
Leonardo de Moura
1d39c2aabc
chore: update stage0
2021-02-01 17:07:10 -08:00
Leonardo de Moura
4a932b9d06
chore: prepare to @ to inductionAlt
2021-02-01 17:05:50 -08:00
Leonardo de Moura
bc173375ba
fix: missing resolveGlobalConstNoOverload
2021-02-01 16:12:25 -08:00
Leonardo de Moura
b4dfa08543
chore: store eliminator name at ElimInfo
2021-02-01 13:16:52 -08:00
Leonardo de Moura
ac104213e3
test: cases-using name resolution issue
2021-02-01 13:16:19 -08:00
Sebastian Ullrich
d4dc54a724
fix: make sure to instantiate mvars in constructors
2021-02-01 12:10:26 +01:00
Sebastian Ullrich
eedce252ff
chore: Nix: do not set extra cmake flags like fsanitize for stage 0
2021-02-01 11:58:37 +01:00
Leonardo de Moura
752af03899
chore: update stage0
2021-01-31 12:10:08 -08:00
Leonardo de Moura
22a7a9e313
fix: missing lean_inc
2021-01-31 12:07:24 -08:00
Leonardo de Moura
f9ebfb466f
fix: missing lean_inc
2021-01-31 11:18:57 -08:00
Leonardo de Moura
d8ced44ce2
test: fix test
...
Error is now caught by the elaborator too
2021-01-31 09:01:08 -08:00
Leonardo de Moura
60805b5c0c
test: test for Int.mod bug
2021-01-31 08:57:41 -08:00
Leonardo de Moura
c4cfbceb71
test: div0 crash
2021-01-31 08:52:39 -08:00
Leonardo de Moura
9419b178bc
chore: update stage0
2021-01-31 08:52:24 -08:00
