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

6033 commits

Author SHA1 Message Date
Leonardo de Moura
f4eb6a4e27 test: heterogeneous + and * 2020-11-30 17:05:57 -08:00
Leonardo de Moura
b6f242434d fix: fixes #229 2020-11-30 11:51:13 -08:00
Sebastian Ullrich
f6816a0ffa refactor: move & split Lean.Delaborator 2020-11-30 13:52:46 +01:00
Leonardo de Moura
4ef7d83445 test: bundled structures 2020-11-29 18:58:42 -08:00
Leonardo de Moura
b66dd397f8 test: CommGroup example 2020-11-29 18:21:59 -08:00
Leonardo de Moura
482f44deda test: basic algebra classes 2020-11-29 17:26:30 -08:00
Leonardo de Moura
384ba49d8e chore: fix tests 2020-11-29 17:05:43 -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
e562959682 feat: add support for auto bound implicits to the structure command 2020-11-29 14:39:51 -08:00
Leonardo de Moura
cb3a2f7947 test: add coercion pullback example from "Hints in Unification" 2020-11-29 08:46:45 -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
05fc1e8bbf feat: optional name for unification hints 2020-11-29 08:05:26 -08: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
249d79218c test: CoeFun 2020-11-28 17:46:00 -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
e21b4a6399 feat: nicer syntax for unification hints 2020-11-27 19:18:18 -08:00
Leonardo de Moura
ebba9d119d feat: unification hints 2020-11-27 18:12:49 -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
3f720d778c fix: unnecessary unfolding 2020-11-27 13:08:18 -08:00
Leonardo de Moura
f2ae695e14 test: propagateExpectedType 2020-11-27 12:17:23 -08:00
Leonardo de Moura
58f1f512f1 feat: simplify heuristics at propagateExpectedType 2020-11-27 12:13:29 -08:00
Leonardo de Moura
93cc8a6403 chore: fix test 
It was working for the wrong reasons
 2020-11-27 09:00:11 -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
2c38cb56ea test: unbundled ConstantFunction 2020-11-26 09:48:12 -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
6f0919f08d chore: fix places that require erewrite 2020-11-25 11:02:26 -08:00
Leonardo de Moura
e3fb7010f1 chore: fix tests 2020-11-25 09:25:45 -08:00
Sebastian Ullrich
de20b14366 feat: delaborate basic do 
/cc @leodemoura
 2020-11-25 16:00:56 +01:00
Sebastian Ullrich
b22e035b6f fix: pretty print empty matchers as nomatch 
/cc @leodemoura
 2020-11-25 11:30:24 +01:00
Sebastian Ullrich
cf9a2ae6af feat: formatter: preserve comments 2020-11-25 11:30:24 +01:00
Sebastian Ullrich
727816e7fd test: bring back Reformat.lean on abbreviated copy of Prelude.lean 
/cc @leodemoura
 2020-11-25 11:30:24 +01:00
Leonardo de Moura
b72a3c69b6 fix: ambiguity at induction/cases 
See efc3a320fe
 2020-11-24 14:59:12 -08:00
Leonardo de Moura
5585f9823f chore: cleaner structure/class syntax 
@Kha I implemented the syntax for structure/class that we discussed this morning.
It is much cleaner. See new tests at `struct2.lean`.
I updated the documentation to use it.
 2020-11-24 13:07:43 -08:00
Leonardo de Moura
3eaa4518a0 test: dependent pattern matching 2020-11-24 11:06:49 -08:00
Leonardo de Moura
8f1ad0411d fix: fixes #220 and #223 2020-11-24 10:18:02 -08:00
Leonardo de Moura
f37fd97d9f chore: fix test 2020-11-23 18:34:38 -08:00
Leonardo de Moura
5884b9c19a feat: add support for instance ... where 
@Kha The fields are not mutually recursive yet, but it is good enough
 for writing examples in the manual.

See new test
 2020-11-23 18:07:02 -08:00
Leonardo de Moura
ac85650e0a feat: add optional where clause at declarations 
closes #191

@Kha Note that it expands into a "let rec".
There are many other places where an optional `where`-clause is
useful. We can add them later. It is relatively easy to add support in
other places using the new helper functions
`expandWhereDeclsOpt` and `expandMatchAltsWhereDecls`
 2020-11-23 12:04:51 -08:00
Leonardo de Moura
f7279ee419 test: add tests for some Lean3 issues 2020-11-23 09:55:39 -08:00
Leonardo de Moura
da3e3211a0 feat: refine propagateExpectedType 2020-11-22 10:16:41 -08:00
Leonardo de Moura
8ed3b8c55f fix: tryPureCoe? 2020-11-22 08:24:56 -08:00
Leonardo de Moura
8598dde6e6 fix: if-then-else elaboration issue 
@Kha I hate this kind of hack, but the behavior looked unacceptabled
to me. I added a big comment describing the issue and the hack.
 2020-11-21 20:51:28 -08:00
Leonardo de Moura
7496f4377f fix: issues with unbound implicit locals 
This commit also add support for them in the `inductive` command.
 2020-11-21 16:17:38 -08:00
Leonardo de Moura
f220654a27 feat: default instances 2020-11-21 14:44:40 -08:00