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

6227 commits

Author SHA1 Message Date
Sebastian Ullrich
f7decd2d46 fix: go to definition for macro_rules etc. 2021-11-24 11:54:13 +01:00
Leonardo de Moura
a8f4146070 feat: support eta struct recursively 
Addresses issues raised by @gebner at #777
 2021-11-23 17:38:48 -08:00
Gabriel Ebner
7537fa7795 fix: unfold x<y in discrimination tree module 2021-11-23 07:34:51 -08:00
Leonardo de Moura
e15a656fd2 fix: remove @[reducible] annotation from Function.comp and Function.const 
closes #813
 2021-11-23 07:29:25 -08:00
Leonardo de Moura
d685c545b4 feat: eta for structures 2021-11-23 06:21:25 -08:00
Scott Morrison
43315f7f94
fix: correct spacing in the pretty printer 2021-11-23 09:13:31 +01:00
Leonardo de Moura
d9b057af03 fix: fixes #793 2021-11-22 13:28:08 -08:00
Gabriel Ebner
f55649f81b fix: prefer simp lemmas with *higher* priority 2021-11-22 11:52:45 -08:00
larsk21
9028405798 fix: handle _root_ in unresolveNameGlobal with pp.fullNames 2021-11-21 15:23:21 +01:00
larsk21
8cf520209f feat: show fully-qualified name in hover text 2021-11-21 15:23:21 +01:00
larsk21
63f9b37c0a fix: return fully-qualified name in PrettyPrinter when pp.fullNames is set 2021-11-21 15:23:21 +01:00
Sebastian Ullrich
25ebc68b87 fix: emit info tree on command without elaborator 
Fixes #792
 2021-11-16 10:44:17 +01:00
Leonardo de Moura
c67541570f fix: fixes #787 2021-11-15 18:31:57 -08:00
Leonardo de Moura
2a7b33089a fix: transparency settings at simp TC check 
fixes #790
 2021-11-15 18:09:31 -08:00
Leonardo de Moura
4b2fa38cb8 fix: #check_failure command should succeed if there are stuck TC problems 2021-11-15 16:56:55 -08:00
Leonardo de Moura
9a152d2051 fix: use withSynthesize at elabStructInstance 
fixes #783
 2021-11-15 16:45:26 -08:00
Sebastian Ullrich
6e4fcaaea9 fix: produce info tree even on macro or elab failure 2021-11-11 08:39:31 +01:00
Leonardo de Moura
743810b77a feat: use binrel_no_prop% to define == notation 
fixes #764
 2021-11-09 07:46:10 -08:00
Leonardo de Moura
a5b1b8de4f fix: bug at Offset.lean 
Offset equalities should not assume default `Nat` instances for
numerals, `+`, `*`, and `-` have been used.

fixes #755
 2021-11-08 18:27:25 -08:00
Sebastian Ullrich
177d45a752 chore: fail without decreasing proof 2021-11-06 18:29:59 +01:00
Leonardo de Moura
b28f92a9ea feat: improve error message produced by #eval command when it fails to synthesize "eval" instance 
closes #765
 2021-11-05 15:03:57 -07:00
Sebastian Ullrich
03551487ad chore: simplify test 2021-11-05 10:45:27 +01:00
Sebastian Ullrich
6e45685310 fix: propositions should never be considered enum types 2021-11-04 15:27:15 -07:00
Leonardo de Moura
5f119cb54f feat: avoid metavariables at CompletionItems 
Not sure whether it helps or creates more confusion.
Note that we are still using the `?` prefix for metavariables on the
InfoView and hover info.
 2021-10-29 08:01:21 -07:00
Leonardo de Moura
68120b24b8 feat: add docstring to CompletionItem 
closes #746
 2021-10-28 08:14:40 -07:00
Leonardo de Moura
3367501511 fix: inaccessible annotations at isDefEq issue 
Issue was reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Change.20in.20pattern.20matching.3B.20expected.20behaviour.3F/near/259059096

fixes #742
 2021-10-27 09:26:12 -07:00
Gabriel Ebner
61e0eab23f refactor: reimplement ofScientific for floats 2021-10-26 11:51:30 -07:00
Gabriel Ebner
220ec6e42c chore: add more decimals tests 2021-10-26 11:51:30 -07:00
Gabriel Ebner
bfc74decde feat: add info field to Syntax.node 2021-10-26 20:19:27 +02:00
Gabriel Ebner
6063c662de feat: predictable naming for notation 2021-10-26 20:19:27 +02:00
Gabriel Ebner
ce15ea98c5 feat: predictable naming for macro_rules 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
80a73dd903 feat: basic support for definitions at inductive declarations 2021-10-25 12:44:35 -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
78b3b8b1e8 fix: pattern should only match if the head symbols are equal 2021-10-22 14:26:11 -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
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
1bd78590e6 test: for Lean 3 nocomputable issue 
Issue reported at
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/noncomputable.20tainting/near/258174927
 2021-10-19 07:15:55 -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
1d372ed7e3 test: well-founded recursion for unary function 2021-10-19 06:47:59 -07: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
c425397b45 feat: Hashable instances for UInt8 and UInt16 2021-10-18 17:19:39 -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
284177a80a feat: missing instances and getOp for byte/float arrays 2021-10-18 16:54:56 -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
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
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