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

3645 commits

Author SHA1 Message Date
Gabriel Ebner
ce15ea98c5 feat: predictable naming for macro_rules 2021-10-26 20:19:27 +02:00
Gabriel Ebner
babfdb879a feat: add aux_def command 2021-10-26 20:19:27 +02:00
Leonardo de Moura
3d1f682144 feat: missing whnf at checkParamsAndResultType 2021-10-25 13:08:43 -07:00
Leonardo de Moura
57f02804f3 feat: use forallTelescopeReducing 
This is needed now that we allow definitions at `inductive`.
 2021-10-25 13:05:23 -07:00
Leonardo de Moura
3dbd1fd074 chore: style 2021-10-25 13:02:15 -07:00
Leonardo de Moura
2b58cb49c9 feat: use whnf at getResultingUniverse 2021-10-25 12:38:56 -07:00
Leonardo de Moura
851ac3809e feat: extend isInductivePredicate 2021-10-25 12:37:04 -07:00
Leonardo de Moura
83cf5b20a1 fix: simpLet 
Given `let x := v; b`, `simpLet` was using an incorrect local context to simplify `v`.
 2021-10-22 16:29:00 -07:00
Leonardo de Moura
55bbaa55d8 fix: toHeadIndex 2021-10-22 14:54:01 -07:00
Leonardo de Moura
78b3b8b1e8 fix: pattern should only match if the head symbols are equal 2021-10-22 14:26:11 -07:00
Leonardo de Moura
881bf2a088 fix: set zeta to true at pattern conv tactic 2021-10-22 14:14:49 -07:00
Leonardo de Moura
4c335fd660 fix: do not use let_fun notation when pp.notation is set to false 2021-10-22 14:10:37 -07:00
Leonardo de Moura
fbdb68b669 feat: conv in conv 
Featured suggested at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20lambda.20body.20in.20conv/near/257193307
 2021-10-22 13:53:56 -07:00
Sebastian Ullrich
f202c7c322 fix: prefer local search path 2021-10-22 12:48:37 +02:00
Sebastian Ullrich
91f1948f50 fix: Lake search path 2021-10-22 12:30:30 +02:00
Leonardo de Moura
b4a6b4f882 fix: do not consume pretty print hints at isDefEq 
TODO: improve the solution. It is too hackish.

The issue was reported here https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20MData.20and.20unification/near/258352713
 2021-10-20 15:58:56 -07:00
Leonardo de Moura
58430704e5 refactor: move inaccessible? to Expr.lean 2021-10-20 15:54:18 -07:00
Leonardo de Moura
f01a124f18 fix: builtin attribute initialization 
The failure was triggered if a module declared (only) builtin
attributes that do not have any persistent extension associated with
them.

Fixes #726
 2021-10-20 13:55:54 -07:00
Leonardo de Moura
b281295190 chore: cleanup 2021-10-20 13:55:54 -07:00
Leonardo de Moura
b7ff5d3352 fix: make sure unused 'let'-declarations are preserved in WF 2021-10-19 06:51:54 -07:00
Leonardo de Moura
a2bcb1c4c1 fix: typo 2021-10-19 06:47:14 -07:00
Leonardo de Moura
b5e640a423 fix: avoid getMVarType' at cleanup tactic 
`getMVarType'` applies `whnf`
 2021-10-19 06:43:07 -07:00
Leonardo de Moura
e494329fb3 fix: addNonRecPreDefs at WF/Main.lean 2021-10-19 06:43:07 -07:00
Sebastian Ullrich
51a41705cb feat: allow more atoms starting with "`" 2021-10-19 14:10:31 +02:00
Gabriel Ebner
d379cd6853 fix: out-of-bounds array access 2021-10-19 12:13:17 +02:00
Sebastian Ullrich
b3c8ee2923 fix: add Lake to built-in search path 2021-10-19 10:57:13 +02:00
Sebastian Ullrich
6a90b30875 fix: prefer user-given search paths 2021-10-19 10:57:13 +02:00
Leonardo de Moura
67c8e76b08 fix: preserve unused let declarations 
This commit fixes reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unused.20let.20disappears/near/257528105
 2021-10-18 17:40:15 -07:00
Leonardo de Moura
e336ff5f93 feat: indentation sensitiviy for macro and elab commands 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Command.20terminator/near/257674790
 2021-10-18 17:16:09 -07:00
Leonardo de Moura
6b2303b243 fix: bug at tryLemmaCore when numExtraArgs > 1 
Fixes bug reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Simp.20bug.20-.20produces.60application.20type.20mismatch.60/near/257711901
 2021-10-18 13:59:19 -07:00
Sebastian Ullrich
d3cf0b8098 fix: deriving Ord on parameterized types 
Fixes #732
 2021-10-18 10:08:13 +02:00
Wojciech Nawrocki
e843fb7ca5 fix: widget messages 2021-10-17 10:01:23 +02:00
Siddharth Bhat
3374806d0f refactor: eliminate unused ExtractMonadResult.hasBindInst 2021-10-15 06:57:24 -07:00
Sebastian Ullrich
08dbf239a6 chore: server: redundant let 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
674e473c84 feat: server: support LAKE env var 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
6a1897302b chore: server: use exit code to communicate absence of package 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
765ed37409 feat: server: support Lake 2021-10-15 06:56:02 -07:00
Gabriel Ebner
d6ba8e597a feat: add range parameter to getInteractiveDiagnostics 2021-10-11 22:59:47 +02:00
Sebastian Ullrich
e068833e8d fix: register missing simp trace classes 2021-10-11 15:37:56 +02:00
Leonardo de Moura
48a40c4d0a fix: quoteString at EmitC.lean 
Fix issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Incorrect.20escaping.20of.20.5Cr.20.3F/near/257061704
 2021-10-11 06:16:56 -07:00
Leonardo de Moura
002fb7f446 fix: make sure pattern is tried on partial applications 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20lambda.20body.20in.20conv/near/256939753
 2021-10-10 15:47:04 -07:00
Leonardo de Moura
04fae18fe4 fix: make sure stop conv pattern stop at first match 2021-10-10 15:47:04 -07:00
Leonardo de Moura
e8bdb66dda fix: make sure we can match pattern inside binders 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20lambda.20body.20in.20conv/near/256890867
 2021-10-10 15:47:04 -07:00
Leonardo de Moura
fb27537b8e fix: appUnexpander name resolution 
fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Scoping.20for.20delaborator.3F
 2021-10-09 08:29:26 -07:00
Gabriel Ebner
34eda689a1 fix: use eraseMacroScopes on trace classes 2021-10-08 11:13:19 -07:00
Sebastian Ullrich
0a43a9c466 refactor: use JSON to communicate between server & package manager 2021-10-08 11:28:04 +02:00
Leonardo de Moura
697e0ce2db feat: apply cleanup tactic before applying decreasing tactic 
Alternative design: apply it only before reporting a failure.
 2021-10-06 19:56:57 -07:00
Leonardo de Moura
91d2f6d4fc feat: add cleanup tactic 2021-10-06 19:54:28 -07:00
Leonardo de Moura
c02b4f2675 refactor: move to Meta namespace 2021-10-06 19:05:37 -07:00
Leonardo de Moura
def7641926 feat: add helper methods for checking dependencies 2021-10-06 19:04:02 -07:00