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

3363 commits

Author SHA1 Message Date
Leonardo de Moura
5e694d4b69 fix: fixes #536 2021-06-29 18:24:46 -07:00
Leonardo de Moura
90a79a0b06 chore: remove command universes 
Now, `universe` may declare many universes. The goal is to make it
consistent with the `variable` command
 2021-06-29 17:01:07 -07:00
Gabriel Ebner
3cff5ceb99 perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
Sebastian Ullrich
30a0954424 refactor: revert MonadRef changes 2021-06-21 10:17:26 -07:00
Sebastian Ullrich
da4c46370d feat: store elaborator declaration name in info tree 2021-06-21 10:17:26 -07:00
Daniel Selsam
ded51882a0
feat: pp motives and misc delab fixes 2021-06-13 00:06:27 +02:00
Leonardo de Moura
a435f3d641 feat: reduce s.1 =?= v to s =?= ⟨v⟩ if structure has a single field 
This feature was suggested by @dselsam at PR #521.
It closes #509
 2021-06-11 11:23:19 -07:00
Gabriel Ebner
94e299a730 fix: instantiate mvars in rewrite tactic 2021-06-11 10:27:05 -07:00
Reijo Jaakkola
32897440dc
fix: change IO.FS.Handle.read to return empty array at EOF 
Make EOF handling in IO.FS.Handle consistent with EOF handling in
IO.FS.Handle.getLine. Previously returned error at EOF which ended up
causing segmentation fault. Remove the declaration of g_io_error_eof,
since it becomes redundant.

Closes #349
 2021-06-08 13:17:53 +02:00
Daniel Fabian
9200de01ef refactor: fix code review comments. 2021-06-06 06:40:09 -07:00
Daniel Fabian
968ae18f20 fix: deal with params for inductive predicates. 2021-06-06 06:40:09 -07:00
Daniel Fabian
b7ecc1acc3 refactor: Make the non-below version of a premise in the below type for inductive predicates implicit. 
Since it is always fully implied by the below version thereof, it carries no real information and shouldn't be used in pattern matching.
 2021-06-06 06:40:09 -07:00
Daniel Fabian
822c551aa2 test: Add a bunch of test for structural recursion on predicates. 2021-06-06 06:40:09 -07:00
Daniel Fabian
ec6f7d9bd6 feat: Implement structural recursion for inductive predicates. 2021-06-06 06:40:09 -07:00
Daniel Fabian
4b7cb058d3 feat: Add support for inductive types to FromJson and ToJson handlers. 2021-06-05 13:53:10 +02:00
Daniel Fabian
06d1d3ae07 fix: Use UInt64 in deriving handler for Hashable. 2021-06-03 06:38:44 -07:00
Leonardo de Moura
4062dee864 fix: fixes #498 2021-05-31 15:42:13 -07:00
Leonardo de Moura
a247249880 feat: add configuration option for disabling proof irrelevance at MetaM 2021-05-27 13:37:26 -07:00
Leonardo de Moura
b91e22af2b fix: fixes #241 2021-05-22 19:10:07 -07:00
Daniel Fabian
c426a816a1 refactor: Make the non-below version of a premise in the below type for inductive predicates implicit. 
Since it is always fully implied by the below version thereof, it carries no real information and shouldn't be used in pattern matching.
 2021-05-22 18:09:32 -07:00
Leonardo de Moura
28b055463f fix: fixes #471 2021-05-22 15:42:52 -07:00
Leonardo de Moura
edb203ca54 fix: fixes #481 2021-05-21 20:40:26 -07:00
Leonardo de Moura
af4485f40e fix: fixes #482 2021-05-21 19:20:24 -07:00
Leonardo de Moura
8eceb07caf feat: new discriminant refinement procedure 2021-05-21 18:08:11 -07:00
Mac Malone
a6dc9e4ef3 feat: class abbrev now supports a type spec (+ test) 2021-05-20 15:23:30 -07:00
Mac Malone
6c07536b33 feat: simplified, improved class abbrev (+ tests) 2021-05-20 15:23:29 -07:00
Daniel Fabian
42bd44ab82 refactor: Capture environment modification in mkMatcher. 
Doing this allows us to add the declaration in the backtracking case of structural recursion.
 2021-05-20 15:20:16 -07:00
Sebastian Ullrich
a02c6fd3eb chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
Daniel Fabian
ab0ef229ac feat: add getBelowIndices. 2021-05-19 07:28:14 -07:00
Daniel Fabian
91ecbb5b5c feat: Add withMkMatcherInput. 
This is the inverse function to `mkMatcher`, i.e. a way to turn a matcher into an input.
 2021-05-19 07:28:14 -07:00
Daniel Fabian
cf030a1634 refactor: Add MkMatcherInput. 
Since we are going to make `mkMatcher` reversible, it's quite useful to have the input be a `structure`. This way we make sure, that the inverse function always returns the same type as `mkMatcher` needs as input.
 2021-05-19 07:28:14 -07:00
Leonardo de Moura
8bbe6cac02 chore: fix test 2021-05-17 14:47:24 -07:00
Leonardo de Moura
53b2ceea51 fix: missing withoutModifyingState at elabSimpConfig 2021-05-16 13:07:13 -07:00
Leonardo de Moura
ac90052139 feat: add option for controlling how deep we go when trying to discharge simp theorem hypotheses 2021-05-16 12:32:05 -07:00
Leonardo de Moura
a498a64490 chore: disable injectivity theorems generation for big structure tests 
The test was producing a stack overflow in debug mode in CI.
 2021-05-15 21:30:40 -07:00
Leonardo de Moura
5d305faee0 chore: increase threshold for Windows workaround in the previous commit 2021-05-15 21:15:37 -07:00
Leonardo de Moura
3b8b46b16c test: closes #441 2021-05-15 20:37:48 -07:00
Leonardo de Moura
c7096f54a2 feat: injectivity theorems for types defined in the prelude 2021-05-14 18:32:26 -07:00
Leonardo de Moura
ea45d3bd40 fix: fixes #457 2021-05-12 20:45:54 -07:00
Leonardo de Moura
4db3ccaddb feat: type ascription should disable implicit lambdas 2021-05-12 19:29:36 -07:00
Leonardo de Moura
b52edf1259 fix: fixes #452 
The new syntax is similar to `matchAlts` and uses `colGe`.
The first `|` is not optional anymore.
 2021-05-10 17:28:10 -07:00
Leonardo de Moura
4675817a9e fix: projection of string literals 2021-05-07 14:38:21 -07:00
Leonardo de Moura
5fcd08326f fix: bug at reduceRec 2021-05-07 14:21:37 -07:00
Leonardo de Moura
7fc6607611 feat: have ... := ... syntax closer to let 2021-05-06 15:38:57 -07:00
Sebastian Ullrich
e6132d37a5 fix: induction/cases: accept wildcard alternative even if some (but not all) cases have been excluded 2021-05-06 14:28:00 +02:00
Leonardo de Moura
164b26bf01 fix: make sure the resulting array size is equal to the number of binders 
The following code relies on this property
```lean
       for uid in scope.varUIds, x in xs do
          sectionFVars := sectionFVars.insert uid x
```
 2021-05-04 19:46:14 -07:00
Leonardo de Moura
56d5d6c564 chore: fix tests 2021-05-04 15:42:03 -07:00
Leonardo de Moura
1a0fc816b1 feat: rename inaccessible variable names at cases 2021-05-01 21:51:58 -07:00
Leonardo de Moura
a2e8bc0780 feat: use binop% to define arith operators 
closes #382
 2021-04-30 19:40:45 -07:00
Leonardo de Moura
adae6fdb40 fix: tolerate type incorrect terms 
This bug was producing a type error when I was using `set_option trace.Elab true`
 2021-04-29 21:34:15 -07:00