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

7170 commits

Author SHA1 Message Date
Leonardo de Moura
41040a81de fix: auxiliary matcher definitions should be treated as abbreviations 
The motivation is to prevent performance problems such as the one
described at issue #854.

Fixes #854 after a update stage0
 2021-12-07 16:43:20 -08:00
Leonardo de Moura
b0fe1e5d10 feat: add Tomas Skrivan's TC resolution improvement 
This commit implements the TC resolution improvement suggested by
Tomas at #815.

Closes #815.
 2021-12-06 17:46:11 -08:00
Sebastian Ullrich
80c3d88e3e refactor: optimize critical import path 2021-12-06 08:05:24 -08:00
Sebastian Ullrich
2e47a8d5ca test: actually register new benchmark 2021-12-03 09:25:53 +01:00
Leonardo de Moura
b2d88f7bcc fix: bug at saveEqn 2021-12-02 17:38:39 -08:00
Leonardo de Moura
bb768b06cd feat: add PersistentArray.foldrM 2021-12-02 17:17:55 -08:00
Sebastian Ullrich
5869283694 test: new linear solver benchmark by Marc 2021-12-02 17:03:35 +01:00
Leonardo de Moura
c42196440f fix: give preference to non-indices at findRecArg 
fixes #837
 2021-12-01 16:45:19 -08:00
Gabriel Ebner
4964f5eb05 chore: add test 2021-11-30 15:34:54 +01:00
Sebastian Ullrich
465913c391 fix: this must be a keyword 2021-11-29 10:06:15 -08:00
Sebastian Ullrich
531eefb7db chore: adapt syntax 2021-11-29 10:06:15 -08:00
Sebastian Ullrich
a329896e70 feat: refine declaration ranges at instance & example 2021-11-27 07:25:15 -08:00
Sebastian Ullrich
4f15805787 feat: annotate declarations with term infos 2021-11-27 07:25:15 -08:00
Leonardo de Moura
0aa32d643e fix: eta struct and proof irrelevance issue 
see #777
 2021-11-27 07:15:57 -08:00
Leonardo de Moura
2d113e83f9 feat: eta struct support for unit-like datatypes 
For example, given `a b : Unit`, we have that `a` and `b` are
definitionally equal by `etaStruct`.

See #777
 2021-11-26 08:36:25 -08:00
Sebastian Ullrich
e9f7c88299 feat: record doc strings of builtin parsers & elaborators 2021-11-26 17:13:19 +01:00
larsk21
e641ae4eae fix: prefix check in set_option completion 2021-11-26 11:42:54 +01:00
Leonardo de Moura
0fc8c1da77 feat: eta for structures at recursors 
see #777
 2021-11-25 11:31:00 -08:00
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
c6c56b15e1 feat: findSysroot? & reworked initSearchPath 2021-11-20 11:04:39 +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
Sebastian Ullrich
d7b8479760 chore: use configured C++ compiler for foreign test 
Fixes #775
 2021-11-09 09:27:10 +01: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
d5e05f31e4 chore: compiler-dependent test flag 2021-11-06 23:37:19 +01: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
85fb03f22c fix: cannot dynamically link against library that depends on statically linked runtime on Windows 2021-11-04 15:32:07 -07:00
Sebastian Ullrich
697e34e229 test: --load-dynlib 2021-11-04 15:32:07 -07: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