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

7990 commits

Author SHA1 Message Date
Leonardo de Moura
a489bdb107 doc: some doc strings 2022-07-30 21:18:50 -07:00
Leonardo de Moura
a63cb24a38 feat: structure field auto-completion 2022-07-30 14:40:21 -07:00
Leonardo de Moura
83ee9b1a57 feat: auto-completion for dotted identifier notation 2022-07-30 10:21:04 -07:00
Leonardo de Moura
3dfa895bf0 feat: OfNat instance postprocessor 
Closes #1389
 2022-07-30 08:35:45 -07:00
Leonardo de Moura
e6031925c3 fix: bug resolving names when using def _root_. 2022-07-29 19:55:02 -07:00
Leonardo de Moura
1b8cda480f feat: elabAsElim eta-expand when major premises are not provided 2022-07-29 18:31:25 -07:00
Leonardo de Moura
eafd2a88ce chore: simplify Prelude.lean and Core.lean using elabAsElim 2022-07-29 18:13:56 -07:00
Leonardo de Moura
485406cc55 fix: no hover info on _ at fun _ => ... 2022-07-29 14:53:02 -07:00
Leonardo de Moura
a44ae3c0fa fix: ensure elabAsElim does not introduce detached info nodes 2022-07-29 12:27:01 -07:00
Sebastian Ullrich
b027946496 feat: suffix linter messages with option name 2022-07-29 10:31:19 -07:00
Sebastian Ullrich
5e6b2a9460 feat: add 'suspicious unexpander patterns' linter 2022-07-29 10:31:19 -07:00
Sebastian Ullrich
c11bd6fa97 test: fix foreign function signatures 2022-07-29 14:10:15 +02:00
Leonardo de Moura
012cb13f51 feat: add [elabAsElim] elaboration strategy 2022-07-28 20:08:29 -07:00
Leonardo de Moura
a6c53cf974 fix: fixes #1380 2022-07-28 15:14:50 -07:00
Sebastian Ullrich
a2ccf8f122 feat: accept keywords as constructor names 2022-07-28 12:46:28 -07:00
Leonardo de Moura
ee6e2036dd feat: allow relations in Type at Trans 
It addresses issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Calc.20mode/near/291214574
 2022-07-28 10:13:01 -07:00
Sebastian Ullrich
556358e84c chore: Nix: better solution for filtering test output 2022-07-28 17:12:17 +02:00
Leonardo de Moura
10c49d0007 fix: preserve user-facing names and BinderInfo when lifting let-rec declarations 
closes #1377
 2022-07-28 06:36:45 -07:00
Leonardo de Moura
6db01d8e48 perf: simpler isDefEq caching 
We don't try to reuse the cache contents between different `isDefEq`
calls. Thus, we can cache more results and ignore whether the state of
the metavariable context affects them or not.

Closes #1102
 2022-07-27 19:35:45 -07:00
Leonardo de Moura
654a4b0478 fix: add term info at trailing parsers 2022-07-27 18:10:46 -07:00
Leonardo de Moura
6dcba78338 refactor: improve MVarId method discoverability 
See issue #1346
 2022-07-27 17:49:00 -07:00
Leonardo de Moura
d267b38a91 fix: disable "error to sorry" and "error recovery" at failIfSuccess 
closes #1375
 2022-07-27 17:09:34 -07:00
Leonardo de Moura
49ce4408df feat: validate parametric local instances 
Closes #1373
 2022-07-27 16:09:56 -07:00
Leonardo de Moura
c210781af8 refactor: add doc strings, cleanup, and dotted notation friendly API 
See #1346
 2022-07-27 16:01:15 -07:00
Leonardo de Moura
1c770ac8d7 feat: doc strings for declare_syntax_cat 
see #1374
 2022-07-27 13:40:08 -07:00
Leonardo de Moura
635752dd2c feat: add info node from attributes to their parsers 
see #1374
 2022-07-27 06:12:43 -07:00
Leonardo de Moura
ed7f502e54 feat: doc string support for register_simp_attr, register_option, register_builtin_option, declare_config_elab 
see #1374
 2022-07-26 18:46:23 -07:00
Leonardo de Moura
642cf0bc6d feat: add option pp.showLetValues 
closes #1345
 2022-07-26 17:53:34 -07:00
Leonardo de Moura
c22120371e feat: finer-grained term infos for do blocks 
closes #1248
 2022-07-26 15:47:37 -07:00
Leonardo de Moura
43c787d1c6 feat: synthesize implicit structure fields in the structure instance notation 
closes #1305
 2022-07-26 13:24:57 -07:00
Leonardo de Moura
e68e448070 fix: convert inductive type instance implicit parameters to implicit when building SizeOf instance 
It is better for TC resolution since the parameter can be inferred by
typing constraints, and it addresses issue #1373
 2022-07-26 12:42:47 -07:00
Leonardo de Moura
d6f0880d11 feat: add option warningAsError 2022-07-26 05:57:54 -07:00
Leonardo de Moura
385cfa6001 fix: fixes #1372 2022-07-26 05:51:02 -07:00
Leonardo de Moura
db7e546155 fix: Match.unify? 
closes #1361
 2022-07-25 20:30:01 -07:00
Leonardo de Moura
b3b2a07ed0 feat: support dotted notation and named arguments in patterns 2022-07-25 18:19:32 -07:00
Leonardo de Moura
69b7771570 fix: etaArgs and ellipsis at elabAppArgs 
When `..` is used, we should not eta-expand but add `_`s.
 2022-07-25 18:13:32 -07:00
Leonardo de Moura
c418e8d2c5 fix: use useExplicit := false when processing instance ... where ... notation fields 
See new test.
 2022-07-25 16:53:13 -07:00
Leonardo de Moura
c2a13da58d fix: ensure let f | ... and let rec f | ... notations behave like the top-level ones with respect to implici lambdas 
closes #1360
 2022-07-25 16:53:13 -07:00
Sebastian Ullrich
da44604c1b fix: notation delaborator on over-application 2022-07-25 13:42:37 -07:00
Wojciech Nawrocki
12b3573c14 fix: tests 2022-07-25 08:01:27 -07:00
Wojciech Nawrocki
122748ab06 test: strip some more indices 2022-07-25 08:01:27 -07:00
Wojciech Nawrocki
5183887722 test: fix infoTree.lean 2022-07-25 08:01:27 -07:00
Ed Ayers
05f79def8c style: tests/lean/interactive/run.lean 
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
 2022-07-25 08:01:27 -07:00
E.W.Ayers
c4c87ebe55 test: remove unused rpc case from runner 2022-07-25 08:01:27 -07:00
E.W.Ayers
18a3d1a34e fix: widgets are now defined using a UserWidgetDefinition 
To satisfy https://github.com/leanprover/lean4/pull/1238#discussion_r908839474
 2022-07-25 08:01:27 -07:00
Leonardo de Moura
262ac674aa feat: improve runTactic 
It must catch exceptions.
See #1342
 2022-07-25 07:41:50 -07:00
Lars
105bfcc8f0
feat: allow custom ignore functions for the unused variables linter 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2022-07-25 09:16:44 +02:00
Leonardo de Moura
8335a82aed refactor: improve MVarId method discoverability 
See issue #1346
 2022-07-24 21:36:33 -07:00
Leonardo de Moura
d9d893e425 chore: fix test 2022-07-24 18:07:54 -07:00
Leonardo de Moura
b6e9d58537 feat: add [deprecated] attribute 2022-07-24 18:06:03 -07:00