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

28017 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
db89750030 chore: update RELEASES.md 2022-05-04 15:31:57 -07:00
Leonardo de Moura
5aaccc8ebb chore: remove OptionM 2022-05-04 15:30:10 -07:00
Leonardo de Moura
eaea5c4773 chore: update stage0 2022-05-04 15:28:49 -07:00
Leonardo de Moura
c65537aea5 feat: Option is a Monad again 
TODO: remove `OptionM` after update stage0

see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Do.20we.20still.20need.20OptionM.3F/near/279761084
 2022-05-04 15:27:42 -07:00
Leonardo de Moura
04d3c6feeb fix: auto implicit behavior on constructors 2022-05-04 15:04:49 -07:00
Leonardo de Moura
a1af8074c9 feat: improve discriminant refinement procedure 2022-05-04 14:46:43 -07:00
Leonardo de Moura
16ed5a3213 fix: erase_irrelevant.cpp 
It addresses issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/'unreachable'.20code.20was.20reached.20by.20termination.20check/near/281159704
 2022-05-04 08:06:59 -07:00
Leonardo de Moura
94b5a9b460 feat: improve split tactic 2022-05-03 17:46:50 -07:00
Gabriel Ebner
88e26b75b0 fix: actually abort with LEAN_ABORT_ON_PANIC 
The previous null-pointer dereference was UB and therefore optimized
away.
 2022-05-03 09:42:45 -07:00
Sebastian Ullrich
f6e74c677e doc: metaprogramming-arith: deduplicate 2022-05-03 18:38:36 +02:00
Sebastian Ullrich
87431da7b1 doc: metaprogramming-arith: style 2022-05-03 18:38:36 +02:00
Joscha
5749fb1474 fix: search for local refs only in current file 
Fixed by adding the identifier's module as an argument to referringTo.
If the ident is RefIdent.const, this is ignored, but if it is
RefIdent.fvar, referringTo limits its search to the ident's module.
 2022-05-03 16:53:03 +02:00
Sebastian Ullrich
e76a2a6d9e chore: normalize spelling 2022-05-03 10:26:11 +02:00
Leonardo de Moura
94abfdba6c feat: improve implementedBy errors, and relax type matching test 2022-05-02 08:48:15 -07:00
Leonardo de Moura
fe00dd8f29 fix: missing sanitizeNames at msgToInteractiveAux 2022-05-02 07:35:12 -07:00
Sebastian Ullrich
c755aa81bd fix: properly distinguish between internal and public linker flags 2022-05-02 13:53:52 +02:00
Sebastian Ullrich
2f3396e58a fix: non-termination in deduplication of lexical references 2022-05-02 09:51:14 +02:00
Sebastian Ullrich
09e4c00c68 fix: lexical references through x := e and similar macros 2022-05-01 17:46:05 +02:00
Leonardo de Moura
109363bc7e fix: closes #1132 2022-05-01 08:18:30 -07:00
Leonardo de Moura
4eb2cfec46 feat: make sure case' ... => tac does not use done after tac 2022-05-01 07:30:11 -07:00
Leonardo de Moura
03524305db fix: findTag? 
If there is an exact match, return it.
 2022-05-01 07:30:11 -07:00
Sebastian Ullrich
a0678b5f6f refactor: rename confusing Reference.isDeclaration field 2022-05-01 16:21:15 +02:00
Sebastian Ullrich
7512f8ab6e chore: CI: pin setup-msys2 
https://github.com/msys2/setup-msys2/issues/216
 2022-05-01 11:58:58 +02:00
Sebastian Ullrich
952abbf16b chore: remove obsolete workaround 2022-05-01 11:52:53 +02:00
Sebastian Ullrich
4174643dbd perf: optimize withAntiquot parenthesizer 
Doesn't look like we'll get rid of the backtracking anytime soon
 2022-05-01 11:52:53 +02:00
Leonardo de Moura
fa943d3864 chore: update RELEASES.md 2022-04-29 15:59:34 -07:00
Leonardo de Moura
ee0414b026 chore: update stage0 2022-04-29 15:51:47 -07:00
Leonardo de Moura
862492778a test: add deq_correct test from Zulip 2022-04-29 15:50:40 -07:00
Leonardo de Moura
cddf9ddd95 fix: forallAltTelescope heterogeneous equality support 2022-04-29 15:37:20 -07:00
Leonardo de Moura
c19672e99e fix: basic support for the new discriminant equality encoding at split 
TODO: This is a temporary fix. We can do better.
 2022-04-29 15:29:39 -07:00
Leonardo de Moura
c241ef61b1 fix: use HEq (if needed) for encoding h : discr equalities 2022-04-29 15:05:48 -07:00
Leonardo de Moura
351f0deae9 feat: add mkEqHEq 2022-04-29 14:31:36 -07:00
Leonardo de Moura
941ad84ece fix: getMkMatcherInputInContext 2022-04-29 12:44:36 -07:00
Leonardo de Moura
95ea0b92ea chore: fix test 2022-04-29 12:40:32 -07:00
Leonardo de Moura
d4d538cad8 fix: counterexample generation for new match encoding 2022-04-29 12:36:53 -07:00
Leonardo de Moura
ec932e389b chore: fix test 2022-04-29 12:30:45 -07:00
Leonardo de Moura
d3bc963e92 chore: update stage0 2022-04-29 12:20:46 -07:00
Leonardo de Moura
6e1c51dd1a feat: splitter proof for new match encoding 2022-04-29 12:19:24 -07:00
Leonardo de Moura
89441aac2a feat: match equation theorem generation for new h : discr notation encoding 
TODO: splitter theorem generation still needs to be fixed.
 2022-04-29 11:48:25 -07:00
Leonardo de Moura
24417ed466 feat: size, get, get!, getD, and getOp for Subarray 2022-04-29 09:55:45 -07:00
Leonardo de Moura
eac83586c6 chore: remove leftover 2022-04-29 09:10:27 -07:00
Leonardo de Moura
c959c80310 chore: reset local context at correct place 2022-04-29 09:08:44 -07:00
Leonardo de Moura
10d43492ba chore: fix test 2022-04-29 07:17:46 -07:00
Leonardo de Moura
8d9626dab7 feat: delaborate match h : d with ... 2022-04-29 07:17:46 -07:00
Leonardo de Moura
0f7754847d chore: style 2022-04-29 07:17:46 -07:00
Leonardo de Moura
d793d2f0fd feat: adapt elabMatchAltView to handle the new encoding for h : discr = pattern 2022-04-29 07:17:46 -07:00
Leonardo de Moura
7a369848a0 feat: new mkMatcher 
TODO: adjust match elaborator
 2022-04-29 07:17:46 -07:00
Leonardo de Moura
f4b4b14797 refactor: prepare to handle match h: notation at Meta\Match\Match.lean 2022-04-29 07:17:46 -07:00
Sebastian Ullrich
9b4feb3d13 perf: work around missed TCO 2022-04-29 16:16:09 +02:00
Sebastian Ullrich
b450fb8243 chore: CI: use stable Nix 2022-04-29 16:16:09 +02:00