Leonardo de Moura
47b8fa15f1
fix: propagate visibility annotation
2021-08-10 15:34:07 -07:00
Leonardo de Moura
9cd729265e
fix: missing instantiateMVars
2021-08-10 10:04:16 -07:00
Leonardo de Moura
9fe1cd1026
chore: modify default value for option structureDiamondWarning
...
We still have some TODO items, but structure diamond support is
already useful in practice.
2021-08-10 09:24:53 -07:00
Leonardo de Moura
50deae9b8b
feat: copy binderInfo and inferMod from original field
2021-08-10 09:12:58 -07:00
Leonardo de Moura
bc26a9b527
feat: improve copyNewFieldsFrom
2021-08-10 09:08:35 -07:00
Leonardo de Moura
af1cecc641
feat: better error message
2021-08-10 07:46:15 -07:00
Leonardo de Moura
9e5998baf0
feat: register instance/reducible attribute for structuer diamond coercions
2021-08-10 07:16:59 -07:00
Leonardo de Moura
0f184a8c93
fix: binder annotation for class diamond coercions
2021-08-10 06:59:28 -07:00
Leonardo de Moura
bccad8edb1
feat: add coercion to parent structure whose fields having been copied
2021-08-09 19:01:08 -07:00
Leonardo de Moura
97664de3ee
fix: diamonds with dependent fields
2021-08-09 19:01:08 -07:00
Leonardo de Moura
e8403f89b0
fix: ensure field names are atomic
2021-08-09 19:01:08 -07:00
Leonardo de Moura
6f318ddde3
feat: save binderInfo and inferMod ad registerStructure
2021-08-09 19:01:08 -07:00
Leonardo de Moura
f67501a890
chore: cleanup
2021-08-09 19:01:08 -07:00
Leonardo de Moura
3f3e5d9dcb
fix: private field + default value bug
2021-08-09 19:01:08 -07:00
Leonardo de Moura
3896c44b55
chore: fix incorrect comment
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2021-08-09 19:01:08 -07:00
Leonardo de Moura
fdce7a99e1
feat: structure diamonds basic support
...
See TODO in the new comments.
2021-08-09 19:01:08 -07:00
Leonardo de Moura
65aafc070c
chore: remove mkInternalSubobjectFieldName hack
2021-08-03 12:05:10 -07:00
Leonardo de Moura
d864afae91
feat: private fields
...
closes #418
2021-08-02 20:20:21 -07:00
Leonardo de Moura
90047e73e8
feat: cache structure parent names
2021-08-02 18:58:00 -07:00
Leonardo de Moura
635bc78d72
feat: use structure extension to implement Structure.lean
2021-08-02 18:03:20 -07:00
Leonardo de Moura
1ca62e21fd
feat: add environment extension for storing structure field information
2021-08-02 16:17:35 -07:00
Leonardo de Moura
56e247763f
fix: scope of the auto param at fields
2021-07-27 15:22:51 -07:00
Leonardo de Moura
0ccd110eb4
feat: elaborate Term.binderTactic at structure declarations
2021-07-27 14:49:23 -07:00
Leonardo de Moura
1a62826107
chore: cleanup
2021-07-27 12:41:26 -07:00
Leonardo de Moura
dbe0d2d706
feat: automatically generate injectivity theorems
2021-05-14 18:05:04 -07:00
Leonardo de Moura
bf583f6065
chore: add placeholders for mkInjectiveTheorems
...
We can activate them yet since the method is failing when there are
heterogeous equalities in the injectivity theorem type.
2021-05-13 22:36:45 -07:00
Leonardo de Moura
b899447817
refactor: move collectFVars to Meta
2021-03-26 19:16:21 -07:00
Leonardo de Moura
99cd4fa720
feat: refine auto bound implicit locals
2021-03-23 17:33:15 -07:00
Leonardo de Moura
bf8119a5cd
chore: convert keywords to snake_case
...
Again `!` is only for functions that can panic.
2021-03-12 13:34:51 -08:00
Leonardo de Moura
be841a7cad
chore: throwError! => throwError, throwErrorAt! => throwErrorAt
...
@Kha I marked the corresponding methods as `protected`.
I currently can't stand `throw_error`, and I am optimistic about
server highlighting feature you are working on :)
2021-03-11 11:59:45 -08:00
Leonardo de Moura
164577d94e
chore: remove parser! and tparser!
...
The new macros are called "leading_parser` and `trailing_parser`.
cc @Kha
2021-03-11 09:36:58 -08:00
Leonardo de Moura
68143ca8ba
chore: trace[...]! ==> trace[...]
...
@Kha I think this one is a good change, there is no real reason for
using the `!` suffix here.
2021-03-10 18:44:43 -08:00
Leonardo de Moura
8fa1ecde49
fix: throw error when default value contains metavariables
2021-02-20 11:31:56 -08:00
Leonardo de Moura
a264268a63
fix: structure field auto bound implicits
2021-02-20 07:46:55 -08:00
Leonardo de Moura
4e4194af41
feat: add autoBoundImplicit support for structure fields
2021-02-06 17:58:29 -08:00
Leonardo de Moura
75466a7cf3
chore: cleanup
2021-01-26 16:01:46 -08:00
Leonardo de Moura
2b6e3bb696
chore: do not generate SizeOf instance for classes
2021-01-20 17:48:27 -08:00
Leonardo de Moura
4ffc2c93cd
feat: invoke mkSizeOfInstances from structure and inductive commands
2021-01-20 17:07:02 -08:00
Leonardo de Moura
84f78edb31
feat: store declaration ranges
2021-01-11 12:50:11 -08:00
Leonardo de Moura
308c61027a
feat: save doc strings
...
We can now document `let rec` too.
2021-01-10 07:13:33 -08:00
Leonardo de Moura
e74ba14f4c
feat: modify structSimpleBinder parser
...
@Kha It felt odd that we can write
```
map f x := ...
```
in instances, but we had to write
```
map (f x) := ...
```
when setting the field default value in a class.
2020-12-23 08:23:14 -08:00
Leonardo de Moura
7720b843bb
feat: allow users to use binders when setting default value for parent fields
2020-12-23 08:12:29 -08:00
Leonardo de Moura
9c47cfe001
fix: panic message
2020-12-23 07:24:46 -08:00
Leonardo de Moura
df03130927
feat: improve error message
2020-12-22 17:50:26 -08:00
Leonardo de Moura
8c2cb44ac0
fix: error message produced by lean_mk_projections
2020-12-22 17:40:32 -08:00
Leonardo de Moura
0fa262bb93
feat: add priority to InstanceEntry
2020-12-16 10:40:58 -08:00
Leonardo de Moura
04a07c15b9
chore: use deriving Inhabited
2020-12-13 11:57:59 -08:00
Leonardo de Moura
0bbc2ca884
feat: elaborate optDeriving
2020-12-13 09:05:03 -08:00
Leonardo de Moura
0b8edeeadc
chore: use double quoted literals
2020-12-09 17:51:01 -08:00
Leonardo de Moura
ae5aa51712
chore: add explicit discard
2020-12-08 06:18:18 -08:00
