Leonardo de Moura
|
ef308e7f2c
|
chore: remove leftover notation
|
2022-08-15 06:25:35 -07:00 |
|
Leonardo de Moura
|
09c0f43ce5
|
chore: update stage0
|
2022-08-15 06:22:47 -07:00 |
|
Leonardo de Moura
|
d903d85a53
|
chore: prepare to remove have notation leftover
|
2022-08-15 06:21:23 -07:00 |
|
Leonardo de Moura
|
9bafe2f5b5
|
chore: update stage0
|
2022-08-14 11:20:54 -07:00 |
|
Mario Carneiro
|
3b793b949b
|
feat: attributes on notation
|
2022-08-14 11:18:20 -07:00 |
|
Leonardo de Moura
|
126ad49401
|
feat: add stage1 extension for storing LCNF declarations
|
2022-08-14 10:59:36 -07:00 |
|
Henrik Böving
|
afbe296edb
|
doc: doc-strings for CompilerM
|
2022-08-14 09:33:58 -07:00 |
|
Henrik Böving
|
8e29fa88eb
|
fix: address code review for jp checker
|
2022-08-14 09:33:58 -07:00 |
|
Henrik Böving
|
ff9c9032b4
|
feat: join point validator
|
2022-08-14 09:33:58 -07:00 |
|
Leonardo de Moura
|
ed616abfb3
|
fix: hover information and go-to definition for notation defined using binop%
|
2022-08-13 21:34:27 -07:00 |
|
Mario Carneiro
|
b3ba6d4bf7
|
fix: use resolveGlobalConstNoOverloadWithInfo more
|
2022-08-13 18:20:55 -07:00 |
|
Leonardo de Moura
|
7a8c91fe83
|
chore: update stage0
|
2022-08-13 18:15:14 -07:00 |
|
Leonardo de Moura
|
713108b7ba
|
chore: re-enable warningAsError
|
2022-08-13 18:07:30 -07:00 |
|
Leonardo de Moura
|
1e1c231edd
|
chore: update stage0
|
2022-08-13 18:07:30 -07:00 |
|
Leonardo de Moura
|
d87d0f47a6
|
chore: temporarily disable warningAsError
|
2022-08-13 18:07:30 -07:00 |
|
Sebastian Ullrich
|
a2d59b9c93
|
fix: preserve condition position info in if
|
2022-08-13 18:07:30 -07:00 |
|
Sebastian Ullrich
|
81c744b12f
|
chore: update tests
|
2022-08-13 18:07:30 -07:00 |
|
Sebastian Ullrich
|
f117606728
|
fix: replace uses of token antiquotations for setting position ranges with withRef
|
2022-08-13 18:07:30 -07:00 |
|
Sebastian Ullrich
|
ed754725e6
|
fix: discriminant info tree term
|
2022-08-13 18:07:30 -07:00 |
|
Sebastian Ullrich
|
757da9f6f3
|
fix: more accurate invalid shadowin error position
|
2022-08-13 18:07:30 -07:00 |
|
Sebastian Ullrich
|
a91ad198b2
|
fix: set ref in expandMacros like with regular expansion
|
2022-08-13 18:07:30 -07:00 |
|
Leonardo de Moura
|
56ee71fa0b
|
chore: update stage0
|
2022-08-13 18:07:30 -07:00 |
|
Sebastian Ullrich
|
b97a145836
|
fix: annotate all syntax nodes produced by quotations as synthetic
|
2022-08-13 18:07:30 -07:00 |
|
Mario Carneiro
|
b201db4bf7
|
feat: add hover info for quot precheck
|
2022-08-13 17:31:57 -07:00 |
|
Leonardo de Moura
|
5f01746dba
|
chore: update stage0
|
2022-08-13 17:24:58 -07:00 |
|
Mario Carneiro
|
c961cd1310
|
feat: doc comments on notation
|
2022-08-13 17:18:14 -07:00 |
|
Mario Carneiro
|
014db5d6d0
|
doc: relocate doc strings from elab to syntax
|
2022-08-13 17:16:40 -07:00 |
|
Mario Carneiro
|
b0db7deeef
|
doc: documentation for Init.Coe
|
2022-08-13 17:15:49 -07:00 |
|
Henrik Böving
|
0d27c5c5cd
|
doc: doc-strings for the entrypoints of the compiler
|
2022-08-13 17:11:07 -07:00 |
|
Leonardo de Moura
|
745f77c657
|
chore: let x := lcUnreachable .. should not occur in LCNF
|
2022-08-13 16:24:44 -07:00 |
|
Leonardo de Moura
|
6c5638d85b
|
fix: bug at toLCNF
|
2022-08-13 15:22:22 -07:00 |
|
Leonardo de Moura
|
7b440040f8
|
test: add Gabriel's examples
They expose issues in the current code generator
|
2022-08-13 11:51:09 -07:00 |
|
Leonardo de Moura
|
cba5f1b374
|
test: add examples that produce the LCNF "any" type
|
2022-08-13 11:37:35 -07:00 |
|
Leonardo de Moura
|
996968c54c
|
chore: display LCNF declaration type at Compiler.step
|
2022-08-13 11:35:46 -07:00 |
|
Leonardo de Moura
|
d2c0aa4d6d
|
chore: remove dead code
|
2022-08-13 11:24:51 -07:00 |
|
Leonardo de Moura
|
9b1db198af
|
fix: bug at toLCNF
|
2022-08-13 10:30:12 -07:00 |
|
Leonardo de Moura
|
212456720c
|
fix: bug at TerminalCases
`Context.jp?` is not a continuation for the local lambda.
|
2022-08-13 10:15:43 -07:00 |
|
Leonardo de Moura
|
d439160f31
|
fix: missing cases at compatibleTypes
|
2022-08-13 10:03:14 -07:00 |
|
Leonardo de Moura
|
0a423b3699
|
fix: ensure the the terminal expression in let-declaration block is not a lambda
|
2022-08-13 09:47:59 -07:00 |
|
Leonardo de Moura
|
a17d00867f
|
feat: common subexpression elimination
|
2022-08-12 16:52:18 -07:00 |
|
Leonardo de Moura
|
dc69a20893
|
feat: add mapValue
|
2022-08-12 16:38:20 -07:00 |
|
Leonardo de Moura
|
0b585d6f3d
|
fix: bug at Compiler/Check.lean
|
2022-08-12 13:59:56 -07:00 |
|
Mario Carneiro
|
9de477ecf9
|
feat: add more float functions
|
2022-08-12 13:12:59 -07:00 |
|
Chris Lovett
|
50cd7debe1
|
feat: simple uri escaping and unescaping (#1452)
|
2022-08-12 19:56:05 +00:00 |
|
Leonardo de Moura
|
37057fdd31
|
feat: eagerly inline simple join points
|
2022-08-12 11:15:12 -07:00 |
|
Leonardo de Moura
|
84d9c6ed8b
|
fix: bug at TerminalCases.lean
|
2022-08-12 10:59:15 -07:00 |
|
Leonardo de Moura
|
cfbefd993b
|
fix: lambdaBoundedTelescope at Compiler/Check.lean
|
2022-08-12 10:20:54 -07:00 |
|
Mario Carneiro
|
6906a4d1ee
|
feat: generalize ReaderT definitions
|
2022-08-12 08:23:11 -07:00 |
|
Mario Carneiro
|
94f85ae649
|
fix: don't show NaN sign info in Float.toString
|
2022-08-12 08:21:47 -07:00 |
|
Mario Carneiro
|
0738136446
|
feat: add lineEq parser alias
|
2022-08-12 08:15:28 -07:00 |
|