max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
23837 commits 1 branch 0 tags 5.3 GiB
Commit graph

6314 commits

Author SHA1 Message Date
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
Sebastian Ullrich
a3a8d76e96 chore: move pp_options.cpp to Lean 2021-01-27 14:16:12 +01:00
Leonardo de Moura
4fc2aead45 fix: missing checkAssignment at assignToConstFun 
Fixes #297
 2021-01-26 17:33:33 -08:00
Leonardo de Moura
2c05e78728 fix: bug at CheckAssignment 2021-01-26 16:20:41 -08:00
Leonardo de Moura
31680c1255 fix: do not evaluate code containing sorry 
closes #277
 2021-01-26 15:01:53 -08:00
Leonardo de Moura
9d0edab6c3 chore: add issue 297 examples 
The stack overflow reported on this issue has already been fixed.

closes #297
 2021-01-26 08:07:41 -08:00
Sebastian Ullrich
1945ebd275 feat: delaborate sorryAx 2021-01-26 12:08:25 +01:00
Leonardo de Moura
f27ae71231 chore: fix test 2021-01-25 17:22:20 -08:00
Leonardo de Moura
d408c835d2 fix: defaultInstance priorities for Neg Int and OfScientific Float 2021-01-25 13:21:07 -08:00
Leonardo de Moura
b575087859 fix: unfold class projections when using TransparencyMode.instances 2021-01-25 12:30:26 -08:00
Leonardo de Moura
f53e83b182 feat: add options maxHeartbeats and synthInstance.maxHeartbeats 2021-01-24 17:45:50 -08:00
Sebastian Ullrich
446f953461 feat: allow hygienic capture of section variables in quotations 2021-01-24 11:46:04 -08:00
Leonardo de Moura
51de663e2c fix: crash when using TransparencyMode.instances 2021-01-22 14:17:19 -08:00
Leonardo de Moura
8f028a41ae fix: eta-expanded term at levelMVarToParam 
This issue produced a nested inductive datatype that could not be
handled by the kernel. See new test.

Without the fix, the inductive declaration contained the term
```
 ((fun α {n : Nat} (t : Vec α n) => ...) Expr n x)
```
The nested occurrence `Vec Expr n` only becomes explicit after
beta-reduction.
 2021-01-22 14:17:19 -08:00
Wojciech Nawrocki
d9c6a992b5 feat: specify version in waitForDiagnostics 2021-01-22 18:02:31 +01:00
Sebastian Ullrich
8a02dfec4f feat: subsume variables under variable 
/cc @leodemoura
 2021-01-22 14:36:05 +01:00
Leonardo de Moura
7ae861f6bd test: simplify 2021-01-21 18:32:23 -08:00
Leonardo de Moura
d6eb5a9ff2 feat: generate sizeOf equality lemmas for constructors 
TODO: support for nested inductive types.
 2021-01-21 17:44:15 -08:00