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

18403 commits

Author SHA1 Message Date
Mario Carneiro
6e7d76f4d8 fix: typo 2022-02-03 18:21:14 -08:00
Leonardo de Moura
1684cfec83 chore: update lake 2022-02-03 18:09:48 -08:00
Leonardo de Moura
12e2a79170 chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
Leonardo de Moura
e9d85f49e6 chore: remove tryPureCoe? 
Based on the discussion at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/for.2C.20unexpected.20need.20for.20type.20ascription/near/269083574
The consensus seemed to be that "auto pure" is more confusing than its worth.
 2022-02-03 16:25:24 -08:00
Leonardo de Moura
5f74cd4968 feat: add let pat := val | elseCase do-notation 2022-02-03 15:55:03 -08:00
Leonardo de Moura
420f5bb315 fix: hide internal namespaces from autocompletion 
closes #993
 2022-02-03 13:33:27 -08:00
Leonardo de Moura
17eab845ed fix: improve tryPostponeIfMVar 
see #992
 2022-02-03 13:24:19 -08:00
Sebastian Ullrich
22526051e0 fix: install sources to src/lean/, not lib/lean 
Not only is this more semantically appropriate (see e.g.
`/usr/src/{linux,rust,...}` on Debian), it also prevents .ilean files
from Lake tests (which are symlinked into the build directory as part of
`src/` during development) from ending up in the built-in LEAN_PATH and
being watched & loaded by the server.
 2022-02-03 18:20:21 +01:00
Gabriel Ebner
55be278cd7 fix: ensure motive of matches is Bool 2022-02-03 18:17:27 +01:00
Gabriel Ebner
54cff10f3f fix: dependent fields in diamond extensions 2022-02-03 09:17:14 -08:00
Leonardo de Moura
c30380e2fa feat: lift the restriction in congr theorems that all function arguments on the lhs must be free variables 
see #988
 2022-02-02 18:23:18 -08:00
Leonardo de Moura
101fc12b54 feat: partially applied user congruence lemmas 
see #988
 2022-02-02 17:41:21 -08:00
Leonardo de Moura
dbb6dcd9a9 fix: remove irrelevant hypotheses in auto-generated equation theorems 2022-02-02 15:39:51 -08:00
Leonardo de Moura
188f0eb70f fix: splitMatch tactic 
Improve how we compute the motive for match-splitter eliminator.

closes #986
 2022-02-02 15:06:03 -08:00
Leonardo de Moura
d7f085976f feat: add Coe MVarId MessageData 2022-02-02 15:06:03 -08:00
Leonardo de Moura
4a4074baab fix: only generalize when needed at cases 2022-02-02 15:06:03 -08:00
Leonardo de Moura
4fe56d2a9d fix: allow mkElimApp to assign new goals when solving typing constraints 2022-02-02 15:06:03 -08:00
Leonardo de Moura
65e1fc1211 feat: at splitMatch only generalize discriminants that are not FVar 2022-02-02 15:06:03 -08:00
Leonardo de Moura
630bf4e129 chore: update error message for throwNestedTacticEx 2022-02-02 15:06:03 -08:00
Leonardo de Moura
3101b98f50 feat: used nested tactic exception at splitMatch 2022-02-02 15:06:03 -08:00
Sebastian Ullrich
16f6b19e21 fix: silence .ilean load errors 2022-02-02 22:02:15 +01:00
larsk21
ce92672c3a fix: remove explicit Ord Range 2022-02-02 13:03:21 +01:00
larsk21
6cee7a6a31 fix: dedup references in findModuleRefs 2022-02-02 13:03:21 +01:00
larsk21
bc65da2e83 feat: extend handleDocumentHighlight 2022-02-02 13:03:21 +01:00
Leonardo de Moura
b1617fe04c feat: add throwNestedTacticEx 
closes #194
 2022-01-31 16:25:44 -08:00
Leonardo de Moura
ccddd0d932 feat: show proof state/unclosed goal message on empty tactic sequences 
closes #361
 2022-01-31 16:22:08 -08:00
Leonardo de Moura
f02013fd76 fix: induction MetaM tactic 
The major premise may be a let-declaration.

closes #983
 2022-01-31 13:41:38 -08:00
Joscha
d2dcff1f9a refactor: address review comments 2022-01-31 21:36:37 +01:00
Joscha
bfc185e98e fix: don't duplicate definition and declaration requests 2022-01-31 21:36:37 +01:00
Joscha
4545e183d8 fix: go to definition in modified file 2022-01-31 21:36:37 +01:00
Joscha
ccf492b61d feat: implement partial ilean updates 2022-01-31 21:36:37 +01:00
tydeu
768e8f76ec chore: update Lake 2022-01-31 14:31:31 +01:00
Sebastian Ullrich
f9ff9ab3fd doc: move documentation on syntax match semantics to elaborator docstring 2022-01-29 08:40:03 -08:00
Sebastian Ullrich
ce58ded16f fix: syntax match of literals 
Fixes #801
 2022-01-29 08:40:03 -08:00
Gabriel Ebner
7d4ae642fb fix: recursively copy subfields in diamond extends 2022-01-29 08:31:34 -08:00
Wojciech Nawrocki
2d1cea0864 feat: inform server if widgets are available 2022-01-29 10:04:25 +01:00
Leonardo de Moura
3db640e770 chore: avoid Name.quickLt 
`Name.quickLt` uses hash code and may produce counterintuitive results
to users.
 2022-01-28 09:48:50 -08:00
Leonardo de Moura
e5ef61225b fix: missing condition at lpo case 3 2022-01-28 09:47:35 -08:00
Leonardo de Moura
cb4a86ac68 fix: do not validate local eq theorems 
see #973
 2022-01-27 11:50:20 -08:00
Leonardo de Moura
d4d9995952 feat: reject user declared namespaces containing _root 
see #490
 2022-01-26 19:15:45 -08:00
Leonardo de Moura
941a6165e5 chore: cleanup 2022-01-26 18:26:23 -08:00
Leonardo de Moura
a63163e992 feat: do not try to discharge hypotheses at simp when type contains assignable metavariables 
closes #973
see https://github.com/leanprover-community/mathport/issues/70
 2022-01-26 17:57:52 -08:00
Leonardo de Moura
2fff4c42b7 fix: make sure irreducible constants are not unfolded when using the default reducibility setting 2022-01-26 11:55:21 -08:00
Leonardo de Moura
8db923e010 feat: generate error message for simp theorems that are equivalent to x = x 
see #973
see https://github.com/leanprover-community/mathport/issues/70
 2022-01-26 11:16:31 -08:00
Leonardo de Moura
36d7f2a1ea chore: remove dead code 2022-01-26 10:38:46 -08:00
Leonardo de Moura
cf3b8d4eb4 chore: cleanup 
Make the code style more uniform.
We still have a lot of leftovers from the old frontend.
 2022-01-26 09:18:17 -08:00
Leonardo de Moura
f0b502aca6 fix: increase the number of heartbeats at Expr.eqv 
On issue #906, `simp` spends a lot of time checking the cache. This
process is time consuming and doesn't allocate memory. Before this
commit, it would take a long time to get the "maximum number of
heartbeats" error message on the example included in this issue.

Closes #906
 2022-01-26 08:25:33 -08:00
Leonardo de Moura
a10e32f537 fix: check "heartbeats" at simp 2022-01-26 07:50:25 -08:00
Leonardo de Moura
15cca3000a fix: withIncRecDepth was not aborting simp 
It was just making it stop simplification at the current branch.

Now, elaboration is interrupted after a few seconds in the example at
issue #906.

see #906
 2022-01-26 07:48:58 -08:00
Leonardo de Moura
868e95df1b feat: add Exception.isMaxRecDepth 2022-01-26 07:38:38 -08:00