Sebastian Ullrich
75243e7f24
feat: change back seqLeft/Right signature
...
This was originally changed for the sake of `do`, which does not depend on it anymore
2021-02-12 17:08:06 -08:00
Leonardo de Moura
c64d053f9e
test: ite and dite congr test
2021-02-12 16:52:56 -08:00
Leonardo de Moura
8b3c61dbb0
fix: checkAssignment
2021-02-11 16:56:32 -08:00
Sebastian Ullrich
18aaef4d93
chore: fix test
2021-02-11 18:45:06 +01:00
Sebastian Ullrich
8320ab6177
fix: syntax match: check identifiers (using strict equality)
2021-02-11 17:50:05 +01:00
Sebastian Ullrich
a74960a4ab
fix: delaborator: match with shadowing
2021-02-11 11:30:25 +01:00
Leonardo de Moura
896ce41b33
chore: fix test
2021-02-10 12:04:33 -08:00
Leonardo de Moura
2aed9a4ec2
chore: special support for match d with | PUnit.unit => rhs
2021-02-10 09:54:12 -08:00
Leonardo de Moura
16429e393d
test: add dep hd test
...
It has been reported in the general channel that this example
generates problems for the Lean 3 elaborator.
2021-02-08 11:26:23 -08:00
Leonardo de Moura
4e4194af41
feat: add autoBoundImplicit support for structure fields
2021-02-06 17:58:29 -08:00
Leonardo de Moura
023d7605fb
feat: add "transitivity" to "has_loose_bvars_in_domain"
2021-02-06 17:42:38 -08:00
Leonardo de Moura
565f6a9372
chore: fix test
2021-02-06 12:54:53 -08:00
Leonardo de Moura
c984e9be4b
test: for issues #306 and #307
2021-02-06 12:48:43 -08:00
Leonardo de Moura
78fb026201
test: add test for issue #305
...
Issue #305 was fixed by previous commits submitted today for problems
exposed by the `for in` notation based on typeclasses :)
closes #305
2021-02-05 18:15:11 -08:00
Leonardo de Moura
83775b08cb
fix: whnfCore not expanding delayed assignments
2021-02-05 15:14:12 -08:00
Leonardo de Moura
8c0346f00c
feat: improve binrel! macro
2021-02-05 13:28:57 -08:00
Leonardo de Moura
09de37e8e5
chore: improve error message
2021-02-05 12:26:39 -08:00
Leonardo de Moura
10a10b38d8
fix: fixes #303
2021-02-05 07:53:18 -08:00
Leonardo de Moura
53539b1dff
chore: use polymorphic method forIn
2021-02-04 18:13:01 -08:00
Leonardo de Moura
b9f5e2a3ad
chore: fix test output
2021-02-04 17:43:56 -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
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
f780efa476
chore: fix test
2021-02-02 14:01:53 -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
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
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
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
3fa1f355eb
fix: mod implementation
2021-01-31 08:19:32 -08:00
Leonardo de Moura
b7a0bdb9c9
fix: Injection.lean
2021-01-30 11:58:56 -08:00
Leonardo de Moura
d71aab5dc4
fix: allow bigger ctor objects
...
`IR/Checker.lean` is now also checking the maximum number of fields
and scalar size
2021-01-29 18:23:38 -08:00
Leonardo de Moura
3c02f877a8
chore: fix test
2021-01-29 17:13:04 -08:00
Leonardo de Moura
761b64c929
fix: missing occursCheck at SyntheticMVars
...
fixes #301
2021-01-29 17:13:04 -08:00
Sebastian Ullrich
811b90dd0e
feat: option for disabling hygiene
...
/cc @leodemoura
2021-01-29 15:26:06 +01:00
Leonardo de Moura
51699f3a5b
feat: ensure binder names are atomic
2021-01-28 11:27:28 -08:00
Leonardo de Moura
870896ba45
chore: fix test
2021-01-27 18:40:53 -08:00
Leonardo de Moura
f1a0044241
fix: use previously generated sizeOf_spec lemmas to expand rhs
2021-01-27 18:14:25 -08:00
Leonardo de Moura
c47c25cf33
feat: finish sizeOf_spec lemma generation
2021-01-27 17:20:23 -08:00
Leonardo de Moura
17edc1d615
test: inductive types for testing SizeOf.lean
2021-01-27 16:26:03 -08:00
Leonardo de Moura
a0ed2d1738
chore: update tests
2021-01-27 15:17:51 -08:00
Leonardo de Moura
8b3a28dd2b
test: reflection
2021-01-27 12:11:43 -08:00
Sebastian Ullrich
e5a9820830
chore: fix test
2021-01-27 15:04:59 +01:00
Sebastian Ullrich
7e521f0105
chore: remove remaining #lang lean4 in tests
2021-01-27 14:45:31 +01:00
