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

17737 commits

Author SHA1 Message Date
Leonardo de Moura
28d81ee456 fix: do not extract closed terms containing constants being defined 
It may produce crashes during initialization.
 2021-09-30 12:46:38 -07:00
Leonardo de Moura
db5df69db4 fix: bounds check 
fixes #704
 2021-09-30 07:55:10 -07:00
Leonardo de Moura
09d0c93589 feat: declare functions in mutual block using auxiliary fuction defined using WF 2021-09-29 11:24:52 -07:00
Leonardo de Moura
608417b946 fix: check number of explicit variables at induction/cases alternatives when @ is not used 
fixes #690
 2021-09-29 07:39:38 -07:00
Leonardo de Moura
3fed9c9df7 feat: reject partial when if constant is not a function 
fixes #697
 2021-09-28 21:07:14 -07:00
Leonardo de Moura
200a38e20c feat: improve letIdLhs parser 
The extra space is only really needed to distinguish an array update (NIY)
```
let x[i] := ...
```
from a declaration taking an instance argument
```
let f [Monad m] := ...
```

closes #696
 2021-09-28 18:10:25 -07:00
Leonardo de Moura
b85d95b7b6 fix: panic in monadic polymorphic code 
fixes #695
 2021-09-28 17:46:19 -07:00
Leonardo de Moura
d0462153a0 fix: bug at smart unfolding procedure 
It fixes an issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Simplifications.20in.20proofs.2Ftype-checking.20not.20happening.3B.20wh.2E.2E.2E
 2021-09-28 10:45:54 -07:00
Sebastian Ullrich
2be3d97cdd chore: leanc: typo & minor modifications 2021-09-28 14:15:58 +02:00
Leonardo de Moura
4c051896df refactor: sizeofMeasure => sizeOfWFRel 
This commit also makes the first argument of `sizeOfWFRel` implicit.
 2021-09-27 19:06:10 -07:00
Leonardo de Moura
bd98e6a586 feat: refine WellFounded.fix functional F over PSigma.casesOn 2021-09-27 19:06:10 -07:00
Leonardo de Moura
d0391d07c2 feat: use PSigma.casesOn instead of projections at packDomain 
Reason: we want to "refine" the `WellFounded.fix` functional `F` over it.
 2021-09-27 19:06:10 -07:00
Leonardo de Moura
8b79176102 feat: refine WellFounded.fix functional F over Sum.casesOn 2021-09-27 19:06:10 -07:00
Leonardo de Moura
f1be1d5bba feat: add simpProj 
Simplifier for kernel projections.
 2021-09-27 19:06:10 -07:00
Leonardo de Moura
c53d892f22 feat: add Expr.projExpr! 2021-09-27 19:06:10 -07:00
Sebastian Ullrich
ae0308fc04 chore: leanc: do not pass linking flags when not linking, again 2021-09-27 17:40:59 +02:00
Leonardo de Moura
108518aad1 feat: use simp at mkDecreasingProof 2021-09-26 16:32:48 -07:00
Leonardo de Moura
d13bdef6e2 feat: add WF.mkFix 2021-09-26 16:01:07 -07:00
Leonardo de Moura
a7f36cc642 chore: style 2021-09-26 15:52:13 -07:00
Leonardo de Moura
094b70c3d4 feat: add notation for Sum and PSum 2021-09-25 18:24:27 -07:00
Leonardo de Moura
dc5f44edcf feat: delaborate Sigma and PSigma 2021-09-25 18:19:44 -07:00
Leonardo de Moura
9d69189a60 chore: use Sum instead of PSum at PackMutual 2021-09-25 17:24:56 -07:00
Leonardo de Moura
d4509878bb feat: add WellFoundedRelation for termination_by 2021-09-25 17:21:03 -07:00
Leonardo de Moura
ceb9889b0e feat: elaborate temination_by term 2021-09-25 16:54:41 -07:00
Leonardo de Moura
a5b27952b5 fix: panic messages on invalid input 
fixes #689
 2021-09-25 09:01:01 -07:00
Leonardo de Moura
1282fb2d97 fix: getMatchWithExtra 
`getMatchKeyArgs` returns arguments in reverse order.
 2021-09-25 08:36:12 -07:00
Leonardo de Moura
4a8679a57c feat: add Subarray.popFront 2021-09-25 08:35:41 -07:00
Sebastian Ullrich
816dc1895f perf: reuse idle thread in favor of spawning new one 2021-09-25 07:34:12 -07:00
Sebastian Ullrich
e6927253cf feat: use leanc written in Lean for testing & distribution 
building is still handled by a (minimal) Bash script for bootstrapping purposes
 2021-09-25 09:59:50 +02:00
Sebastian Ullrich
a9c5eb491d chore: put import library in lib/lean/ 2021-09-25 09:59:50 +02:00
Sebastian Ullrich
a8207e52a9 chore: remove unused flag 2021-09-23 16:32:55 +02:00
Sebastian Ullrich
70f99ab655 chore: placate GCC 2021-09-23 16:31:41 +02:00
Leonardo de Moura
58c938cef8 feat: 'termination_by' goodies 2021-09-22 21:09:33 -07:00
Leonardo de Moura
8425a53377 feat: improve termination_by notation 2021-09-22 21:08:01 -07:00
Leonardo de Moura
38f91a2fa4 doc: PackMutual.lean 2021-09-22 18:27:57 -07:00
Leonardo de Moura
0b7b174f25 feat: replace recursive applications at packMutual 2021-09-22 18:07:07 -07:00
Leonardo de Moura
b8454f3568 fix: packDomain 2021-09-22 18:00:22 -07:00
Leonardo de Moura
65983ef45b feat: add WF/PackMutual.lean 2021-09-22 15:46:47 -07:00
Sebastian Ullrich
d506b8a5ed feat: hide non-exported symbols on Unix 2021-09-22 23:02:39 +02:00
Sebastian Ullrich
ea244c298c chore: un-orphan file 2021-09-22 16:04:18 +02:00
Chris Lovett
ad7c5b26a7
fix: UTF-8 file path support for lean on Windows 
* fix msys2 windows build so the windows apps support utf-8 file paths.

* use windres to compile default-manifest.o

* windres is in binutils.

* stop modifying default-manifest.o

* copy to stage0

* fix semicolon joining of lists in add_custom_target

* undo changes to stage0 as per CR feedback.

* fix makefile

* fix: revert cmakelists.txt COMMAND_EXPAND_LISTS  change

* fix: msys2 dependencies

* add unit test for decoding UTF-8 chars to prove "lean.exe" can read utf-8 encoded files where utf-8 is also used in the file name.

* fix: utf-8 test by using windows-2022

* fix: do we really need cmake 3.11 or will 3.10 do?

* nope, really does require cmake 11.
 2021-09-22 12:21:52 +02:00
Leonardo de Moura
07fb8504a1 fix: bug introduced today 2021-09-21 20:36:18 -07:00
Leonardo de Moura
a909e8cf26 feat: arity mismatch error message at well-founded recursion 2021-09-21 20:34:15 -07:00
Leonardo de Moura
ed47091691 chore: add extra trace messages and document issue 2021-09-21 20:33:44 -07:00
Leonardo de Moura
c41b3d6928 fix: reset local context at addPreDefinitions 2021-09-21 20:18:59 -07:00
Leonardo de Moura
ee2bdc1f84 feat: add WF/PackDomain.lean 2021-09-21 19:38:43 -07:00
Leonardo de Moura
6a880fecc9 chore: modify findDocString? 2021-09-21 17:29:40 -07:00
Leonardo de Moura
5a301d8c3b refactor: add src/Lean/Elab/PreDefinition/WF directory 2021-09-21 15:44:21 -07:00
Leonardo de Moura
640fc964b6 feat: basic termination_by bookkeeping 2021-09-21 15:24:42 -07:00
Leonardo de Moura
6211b95e06 feat: add termination_by parser 2021-09-21 13:19:01 -07:00