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

15282 commits

Author SHA1 Message Date
Sebastian Ullrich
6cef5f17b7 chore: prepare moving Lean.Delaborator into Lean.PrettyPrinter 2020-11-30 13:39:18 +01:00
Leonardo de Moura
72215c7144 feat: add TransparencyMode.instances 2020-11-29 18:12:33 -08:00
Leonardo de Moura
d734a2605b chore: adjust stdlib 2020-11-29 17:01:56 -08:00
Leonardo de Moura
40e51270f5 feat: add withReducible <tacticSeq> 
Use `try (withReducible rfl)` after `rw` and `erw`
 2020-11-29 16:52:30 -08:00
Leonardo de Moura
390eea3750 feat: use One and Zero classes when expanding numeric literals 2020-11-29 16:23:52 -08:00
Leonardo de Moura
89961a608e fix: missing withDeclName 2020-11-29 16:22:11 -08:00
Leonardo de Moura
da15bc27c6 feat: add Zero and One classes 2020-11-29 16:02:34 -08:00
Leonardo de Moura
e562959682 feat: add support for auto bound implicits to the structure command 2020-11-29 14:39:51 -08:00
Leonardo de Moura
dfd1f23030 fix: avoid unnecessary page allocation 
When import objects deleted by other threads, we may add elements to
`p` free list.
 2020-11-29 13:33:59 -08:00
Leonardo de Moura
6dd3616298 fix: import pending objects *before* moving segments 
@Kha I stopped getting the assertion violation after this fix.
There is another unrelated issue that I will fix in a separate commit.
 2020-11-29 13:26:10 -08:00
Sebastian Ullrich
a22d234e93 fix: Thunk.get: mark result as MT before storing it in the task object 2020-11-29 18:59:39 +01:00
Sebastian Ullrich
65c1bc8952 fix: gen_constants_cpp.py: mark constants as persistent 2020-11-29 18:59:39 +01:00
Leonardo de Moura
9e860672ad chore: helper trace message 2020-11-29 08:46:34 -08:00
Leonardo de Moura
df665eb8fc fix: notation 2020-11-29 08:28:01 -08:00
Leonardo de Moura
e9069b6965 feat: expand optional priority at notation and mixfix commands 2020-11-29 08:22:47 -08:00
Leonardo de Moura
ee5679c77c chore: prepare to add optional priorities to the notation and mixfix commands 2020-11-29 08:05:26 -08:00
Leonardo de Moura
05fc1e8bbf feat: optional name for unification hints 2020-11-29 08:05:26 -08:00
Sebastian Ullrich
f649f24014 fix: compilation on Windows 2020-11-29 14:08:53 +01:00
Sebastian Ullrich
c0f94c902e fix: memory leak in interpreter 2020-11-29 14:08:53 +01:00
Leonardo de Moura
2ffd929227 feat: improve unification hints 
The constraints don't need to be in the same universe anymore.
The new test demonstrates why this is useful.
 2020-11-28 19:03:21 -08:00
Leonardo de Moura
16003871e4 feat: add helper instance 2020-11-28 19:01:54 -08:00
Leonardo de Moura
5ead7bfc81 feat: add [elabWithoutExpectedType] attribute 2020-11-28 13:23:37 -08:00
Leonardo de Moura
470717ba67 feat: autoBoundImplicit for universes 2020-11-28 12:45:57 -08:00
Leonardo de Moura
5a396a4872 feat: insert auto bound implicit arguments before explicitly provided ones 
cc @Kha
 2020-11-28 12:45:57 -08:00
Leonardo de Moura
0b8b30ef9e fix: CoeFun and CoeSort perf issue 2020-11-28 12:45:57 -08:00
Leonardo de Moura
4fc32d114f chore: "unbound implicit" => "auto bound implicit" 2020-11-28 12:45:57 -08:00
Leonardo de Moura
b6f2ed9e78 feat: add instances for converting CoeFun and CoeSort into Coe 2020-11-28 12:45:57 -08:00
Sebastian Ullrich
99383d97e1 feat: measure interpreter time & fix enabling interpreter traces 2020-11-28 17:36:20 +01:00
Sebastian Ullrich
b41301747d chore: fall back to raw printer on pretty printing failure 
/cc @leodemoura
 2020-11-28 17:36:20 +01:00
Sebastian Ullrich
2a5c85d9e3 refactor: inline FormatMacro 
@leodemoura: This was just a remnant of the initial frontend porting, correct?
 2020-11-28 12:37:36 +01:00
Sebastian Ullrich
1bcc8f7c16 chore: parenthesizer: more helpful panic message 2020-11-28 12:37:35 +01:00
Sebastian Ullrich
3c86f79bad fix: one instance of parenthesizer "visiting a syntax tree without precedences" 2020-11-28 12:37:35 +01:00
Leonardo de Moura
e21b4a6399 feat: nicer syntax for unification hints 2020-11-27 19:18:18 -08:00
Leonardo de Moura
3d3bed56fd feat: add alias bracketedBinder 2020-11-27 19:01:26 -08:00
Leonardo de Moura
ebba9d119d feat: unification hints 2020-11-27 18:12:49 -08:00
Leonardo de Moura
0869f38de4 chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Wojciech Nawrocki
b1e6edefde fix: redirect child I/O to null on Process.Stdio.null 
And don't use errno for Win32 API errors.
 2020-11-27 13:17:32 -08:00
Leonardo de Moura
5981553e11 chore: remove workaround 2020-11-27 13:15:31 -08:00
Leonardo de Moura
3f720d778c fix: unnecessary unfolding 2020-11-27 13:08:18 -08:00
Leonardo de Moura
c0db9f1e0c chore: adjust stdlib to recent changes 2020-11-27 12:26:07 -08:00
Leonardo de Moura
58f1f512f1 feat: simplify heuristics at propagateExpectedType 2020-11-27 12:13:29 -08:00
Leonardo de Moura
d212a5b671 feat: add macro withoutExpectedType! <term> 2020-11-27 11:08:58 -08:00
Leonardo de Moura
09ed75f517 feat: remove restriction from propagateExpectedType 2020-11-27 09:14:26 -08:00
Leonardo de Moura
fcc382df08 fix: improve Offset.lean 
It did not support for assigned metavariables.
 2020-11-27 08:40:43 -08:00
Leonardo de Moura
2909313475 fix: doLetArrow and doReassignArrow 
@Kha the new tests did not work without this fix.
The `| _ =>` was being parsed as part of the `doLetArrow` and `doReassignArrow`
 2020-11-26 10:29:08 -08:00
Leonardo de Moura
43d98ef7e3 fix: Term/Sort parsers 
missing `checkColGt`
 2020-11-26 09:34:32 -08:00
Leonardo de Moura
8898988747 fix: namespace resolution 2020-11-26 08:17:35 -08:00
Leonardo de Moura
eabbb6eca0 feat: improve [defaultInstance] 
cc @Kha
 2020-11-25 18:33:06 -08:00
Leonardo de Moura
975271e1a3 feat: hide inaccessible names and add pp.inaccessibleNames 
@Kha We will probably have to refine the heuristic for hiding the
inaccessible names, but the first version is already useful.
Here is the error message for a `_` before this commit
```
error: don't know how to synthesize placeholder
context:
x✝⁴ : List Nat
x✝³ : Nat
x✝² : x✝⁴ ≠ []
a b x✝¹ : Nat
x✝ : [a, b] ≠ []
⊢ Nat
```
After
```
error: don't know how to synthesize placeholder
a b : Nat
 : [a, b] ≠ []
⊢ Nat
```
 2020-11-25 17:22:09 -08:00
Leonardo de Moura
276a8b99dd refactor: move ppGoal to Meta 
We need `MetaM` methods such as `isProp` to improve `ppGoal`.
This commit also moves `currNamespace` and `openDecls` to
`Core.Context`. Without this change, `Meta.ppExpr` was not taking
`open` commands into account.
 2020-11-25 14:17:13 -08:00