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

8611 commits

Author SHA1 Message Date
Mario Carneiro
82196efe94 feat: hovers on open and export decls 2023-11-02 17:01:51 +01:00
Mauricio Collares
cfe5a5f188
chore: change simp default to decide := false (#2722) 2023-11-02 10:06:38 +11:00
Leonardo de Moura
db281f60fe
fix: fixes #2178 (#2784) 2023-10-30 15:06:56 +11:00
Scott Morrison
7286dfa38a
feat: withAssignableSyntheticOpaque in assumption (#2596) 
* feat: withAssignableSyntheticOpaque in assumption
* add test
 2023-10-30 04:00:52 +00:00
thorimur
50f2154cbb
fix: make rw [foo] look in the local context for foo before it looks in the environment (#2738) 2023-10-30 14:08:02 +11:00
Joachim Breitner
f74ae5f9c0
feat: Array.mem: Avoid DecidableEq, set up decreasing_trivial (#2774) 
The notation `a ∈ as` for Arrays was previously only defined with
`DecidableEq` on the elements, for (apparently) no good reason. This
drops this requirements (by using `a ∈ as.data`), and simplifies a bunch
of proofs by simply lifting the corresponding proof from lists.

Also, `sizeOf_lt_of_mem` was defined, but not set up to be picked up by
`decreasing_trivial` in the same way that the corresponding List lemma
was set up, so this adds the tactic setup.

The definition for `a ∈ as` is intentionally not defeq to `a ∈ as.data`
so that the termination tactics for Arrays don’t spuriously apply when
recursing through lists.
 2023-10-30 13:47:30 +11:00
Kyle Miller
5fc079d9ce
fix: dsimp missing consumeMData when closing goals by rfl (#2776) 
Fixes #2514
 2023-10-30 09:32:32 +11:00
Leonardo de Moura
dbcc7966cf test: for simp [x] where x is a let-variable 2023-10-25 03:12:35 -07:00
Leonardo de Moura
3b831271ee fix: fixes #2669 #2281 2023-10-25 03:12:35 -07:00
Leonardo de Moura
3a13200772 refactor: add configuration options to control WHNF 
This commit also removes parameter `simpleReduce` from discrimination
trees, and take WHNF configuration options.
Reason: it is more dynamic now. For example, the simplifier
will be able to use different configurations for discrimination tree insertion
and retrieval. We need this feature to address issues #2669 and #2281

This commit also removes the dead Meta.Config field `zetaNonDep`.
 2023-10-25 03:12:35 -07:00
thorimur
6063deb6bd
fix: rw ... at h unknown fvar bug (#2728) 2023-10-25 01:52:19 +00:00
thorimur
291e95e3c5
fix: add instantiateMVars to replaceLocalDecl (#2712) 
* fix: `instantiateMVars` in `replaceLocalDecl`
* docs: update `replaceLocalDecl`
* test: `replaceLocalDecl` instantiates mvars
 2023-10-25 10:26:09 +11:00
Buster Copley
bccbefdc1c
fix: version numbers in code actions (#2721) 
Co-authored-by: Richard Copley <buster@buster.me.uk>
 2023-10-24 22:55:47 +11:00
Leonardo de Moura
b00c13a00e
chore: remove "paper cut" when using Fin USize.size (#2724) 2023-10-24 21:06:35 +11:00
Leonardo de Moura
a7323c9805 feat: use forall_prop_domain_congr in simp tactic 
closes #1926
 2023-10-23 06:19:19 -07:00
Leonardo de Moura
0bd15be1a1 chore: fix tests output 2023-10-22 06:48:22 -07:00
Leonardo de Moura
9a7565d66c perf: closes #2552 2023-10-22 06:48:22 -07:00
thorimur
1facbde113 test: ensure dsimp can use rfl thm constants 2023-10-20 19:06:40 -07:00
Scott Morrison
1e74c6a348
feat: use nat_gcd in the kernel (#2533) 
* feat: use nat_gcd in the kernel

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2023-10-15 13:49:41 +11:00
Scott Morrison
66ab016723
chore: simp tracing reports ← (#2621) 
* chore: simp tracing reports ←

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
 2023-10-15 12:12:10 +11:00
Arthur Adjedj
ff20a14c69
fix : make mk_no_confusion_type handle delta-reduction when generating telescope (#2501) 
* fix : make `mk_no_confusion_type` handle delta-reduction when checking the inductive type.

* tests: extend `2500.lean`
 2023-10-14 17:18:37 +11:00
Mario Carneiro
6bdfde7939 fix: quot reduction bug 2023-10-11 21:25:34 -07:00
Scott Morrison
57e23917b6 fix: implementation of Array.anyMUnsafe 
move test
 2023-10-11 11:20:45 +02:00
Scott Morrison
833e778cd5
chore: add axiom for tracking use of reduceBool / reduceNat (#2654) 2023-10-11 01:47:59 +00:00
Scott Morrison
ca0e6b0522
chore: fix MVarId.getType' (#2595) 
* chore: fix MVarId.getType'

* add test
 2023-10-09 11:04:33 +00:00
Sebastian Ullrich
00e981edcd perf: do not inhibit caching of default-level match reduction 2023-10-08 17:24:20 -07:00
int-y1
ce4ae37c19 chore: fix more typos in comments 2023-10-08 14:37:34 -07:00
int-y1
8d7520b36f chore: fix typos in comments 2023-10-08 10:46:05 +02:00
David Christiansen
b0b922bae4 feat: list the valid case tags when the user writes an invalid one 
Before, Lean would simply emit the message "tag not found". With this
change, it also tells the user what they could have written that would
be accepted.
 2023-10-06 11:14:21 +02:00
Mario Carneiro
89b65c8f1d
feat: make Environment.mk private (#2604) 
* feat: make `Environment.mk` private

---------
 2023-10-04 22:02:54 +11:00
Alexander Bentkamp
7dc1618ca5
feat: Web Assembly Build (#2599) 
Co-authored-by: Rujia Liu <rujialiu@user.noreply.github.com>
 2023-10-04 09:04:20 +02:00
kuruczgy
83c7c29075
fix: XML parsing bugs (#2601) 
* fix: make XML parser handle trailing whitespace in opening tags

* fix: make XML parser handle comments correctly

---------

Co-authored-by: György Kurucz <me@kuruczgy.com>
 2023-10-04 11:51:22 +11:00
Alex J Best
44bc68bdc6
fix: withLocation should use withMainContext for target (#2607) 2023-10-04 10:12:43 +11:00
Arthur Adjedj
6b93f05cd1
feat : derive DecidableEq for mutual inductives (#2591) 
* feat : derive `DecidableEq` for mutual inductives

* doc: document `RELEASES.md`

---------
 2023-10-03 02:17:13 +00:00
Joachim Breitner
ae470e038e
docs: fix doc comment syntax in declModifiers doc comment (#2590) 
The hover on `declModifiers` says doc comments are `/-! … -/`, when it
should say `/-- … -/`.
 2023-09-27 11:57:40 +10:00
Mario Carneiro
e6fe3bee71 fix: hover term/tactic confusion 2023-09-26 10:16:37 +02:00
tydeu
2ac782c315 test: lake: add env & dep cfg benchmarks + cleanup 2023-09-22 20:31:48 -04:00
Sebastian Ullrich
c3fd34f933 chore: disable "lake build lean" benchmark for now 2023-09-22 20:05:20 +02:00
Mac Malone
57fb580a71 doc: fix Inundation README typo 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2023-09-22 20:05:20 +02:00
tydeu
00efb7eaca test: add reconfigure benchmark 2023-09-22 20:05:20 +02:00
tydeu
5b2e3e2b0a test: make compatible with olean caching 2023-09-22 20:05:20 +02:00
tydeu
8dba187910 chore: inundation for configure benchmark 2023-09-22 20:05:20 +02:00
tydeu
7c2ca92661 doc: improve inundation README 2023-09-22 20:05:20 +02:00
tydeu
1d51492139 test: lake: add build Init/Lean/Lake benchmark 2023-09-22 20:05:20 +02:00
tydeu
9a0e57c721 test: add lake benchmarks 2023-09-22 20:05:20 +02:00
Arthur Adjedj
325fab1c1d
fix: don't try to generate below for nested predicates. (#2390) 
* fix: don't try to generate `below` for nested predicates.

* doc : document test #2389

* doc : document `mkBelow`

* test: extend `2389.lean`

* style: fix comments in `IndPredBelow.lean` and `2389.lean`
 2023-09-21 14:24:37 +10:00
thorimur
e79370a1e6
fix: only return new mvars from refine, elabTermWithHoles, and withCollectingNewGoalsFrom (#2502) 
* fix: `withCollectingNewGoalsFrom`
do not collect old goals

* fix: update occurs check

* test: fix test `run/492.lean`

* docs: add docstring to `elabTermWithHoles`

* test: `refineFiltersOldMVars`

* test: fix `expected.out` name

* test: fix `expected.out` filename and line numbers

* docs: use long ascii dash instead of em dash

Co-authored-by: Scott Morrison <scott@tqft.net>

* docs: fix long line, mention lean4#2502

* docs: a couple more long lines

* test: fix line numbers

---------

Co-authored-by: Scott Morrison <scott@tqft.net>
 2023-09-21 14:23:27 +10:00
Sebastian Ullrich
dc60150b5a chore: update domain 2023-09-20 15:13:27 -07:00
Joachim Breitner
b2d668c340
perf: Use flat ByteArrays in Trie (#2529) 2023-09-20 13:22:37 +02:00
Mario Carneiro
f0af71a57b fix: use MoveFileEx for rename on win 2023-09-19 20:24:37 +02:00