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

18368 commits

Author SHA1 Message Date
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
Leonardo de Moura
98407798af fix: mkEquationsFor at Match/MatchEqs.lean 
closes #974
 2022-01-25 18:43:51 -08:00
Leonardo de Moura
a969014eb9 chore: add matchHEq? 2022-01-25 18:43:51 -08:00
Leonardo de Moura
9c293abb9c chore: expose heqToEq tactic 2022-01-25 18:43:51 -08:00
Leonardo de Moura
6547af988b feat: add substVars 2022-01-25 18:43:51 -08:00
Sebastian Ullrich
180cc59d64 chore: update Lake to https://github.com/leanprover/lake/pull/48/files 2022-01-25 23:25:52 +01:00
Sebastian Ullrich
cfaba85199 feat: load precompiled modules in the server 2022-01-25 23:25:52 +01:00
Leonardo de Moura
234f70fadb chore: remove the now incorrect comment 2022-01-24 19:05:05 -08:00
Leonardo de Moura
02677cf326 fix: igore instance implicit arguments in term ordering used at simp 
closes #972
 2022-01-24 18:57:31 -08:00
Leonardo de Moura
d4f7899591 chore: avoid code duplication setting Simp.Config 2022-01-24 18:57:31 -08:00
Leonardo de Moura
722bf54929 fix: trace message with incorrect MetavarContext 2022-01-24 10:34:44 -08:00
Leonardo de Moura
7ada79bf2e fix: use an AC-compatible ordering on Expr at simp 
closes #968
 2022-01-22 09:42:59 -08:00
Leonardo de Moura
763a337c25 chore: helper functions 2022-01-22 09:30:57 -08:00
Leonardo de Moura
0615020cf7 feat: make sure Expr.approxDepth does not overflow 2022-01-22 07:45:19 -08:00
Leonardo de Moura
b0083e0dd0 feat: use elaborated type to generate instance name 
closes #951
 2022-01-20 17:09:55 -08:00
Leonardo de Moura
a9659afa50 chore: remove old decls 2022-01-20 15:35:19 -08:00
Leonardo de Moura
6f416147b4 chore: rename coeM and liftCoeM 2022-01-20 15:33:17 -08:00
Leonardo de Moura
2192e6148b chore: remove coe, coeSort, and coeFun abbreviations 
The notation `↑ e` is now expanded eagerly.

See #403
 2022-01-20 15:19:06 -08:00
Leonardo de Moura
3c17755730 chore: prepare to remove coe definitions 
The notation `↑ e` will eagerly expand the coersion.

See #403
 2022-01-20 15:07:54 -08:00
Leonardo de Moura
f9fa24435d chore: remove problematic instance hasOfNatOfCoe 
See #403
See https://github.com/leanprover-community/mathport/issues/94
 2022-01-20 14:47:25 -08:00
Sebastian Ullrich
f0f26728ed doc: more about initializers 2022-01-20 18:55:57 +01:00
Sebastian Ullrich
52de670497 chore: clarify safety of compile-time code execution 2022-01-20 18:55:57 +01:00
Sebastian Ullrich
c59f7a55cf fix: initialize precompiled modules 2022-01-20 18:55:57 +01:00
Leonardo de Moura
b1a92f5cbf feat: better Repr instances for Level.Data and Expr.Data 
see #619
 2022-01-20 09:45:30 -08:00
Leonardo de Moura
ff4be1e1db feat: add Repr instances for Level and Expr 
closes #619

TODO: a better `Repr` instance for `Expr.Data`
 2022-01-20 09:26:06 -08:00
Leonardo de Moura
d190d6dda4 fix: use default reducibility when proving equation theorems for definition 
Addresses issue reported by @fpfu at #945
 2022-01-20 08:23:51 -08:00
Joscha
9949f92648 refactor: base findModuleWithExt on findWithExt 2022-01-20 17:20:01 +01:00
Joscha
2423a78db4 refactor: implement suggestions 2022-01-20 17:20:01 +01:00
Sebastian Ullrich
3a926b1047 fix: use user-facing private decl name in symbol query 2022-01-20 17:20:01 +01:00
Sebastian Ullrich
53d90a71ae feat: do case-sensitive symbol query if query contains upper-case char 2022-01-20 17:20:01 +01:00
Sebastian Ullrich
1168334cca fix: Unicode symbol lookup 2022-01-20 17:20:01 +01:00
Joscha
7540889bd3 feat: implement LSP workspace symbol request 2022-01-20 17:20:01 +01:00
Leonardo de Moura
f5509ab867 fix: equational lemma generation for definitions using named patterns 
closes #945
 2022-01-19 17:45:54 -08:00
Leonardo de Moura
ef449e816f chore: improve trace messages 2022-01-19 14:29:04 -08:00
Sebastian Ullrich
bbec84bb18 chore: more output on trace.Elab.info 2022-01-19 21:40:29 +01:00
Joscha
3651ebb377 fix: don't send worker notification to client 2022-01-19 16:29:10 +01:00