Leonardo de Moura
d775dc6195
feat: add flag for controlling the execution of initialize commands when importing modules programmatically
...
Fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Environment.20extensions.20in.20importModules
2021-08-16 17:43:28 -07:00
Leonardo de Moura
6ced2cdece
refactor: move lean_name_eq to runtime, add lean_name_hash in C
2021-08-16 16:13:55 -07:00
Leonardo de Moura
14b611af96
refactor: move buffer.h and *_ref.h files to runtime
2021-08-16 15:39:38 -07:00
Leonardo de Moura
571a0491ee
feat: add Meta.byCases helper tactic
2021-08-16 14:58:51 -07:00
Leonardo de Moura
fcbd807c9d
chore: some Expr constructors
2021-08-16 13:58:48 -07:00
Leonardo de Moura
f59b9813fb
feat: add environment extension for caching Simp.Context for splitIf
2021-08-16 13:05:01 -07:00
Leonardo de Moura
34b092700e
feat: add LazyInitExtension
2021-08-16 12:54:50 -07:00
Leonardo de Moura
a3a3c7c80c
chore: add LEAN_PATH_SEPARATOR cmake variable
...
Motivation: try to fix failure at 81ff285427
2021-08-16 10:50:01 -07:00
Leonardo de Moura
ca0c205389
feat: add registerSimpAttr
2021-08-16 09:59:58 -07:00
Leonardo de Moura
81ff285427
chore: use leanmake instead of leanpkg
2021-08-16 08:52:27 -07:00
Leonardo de Moura
9182ebd4c1
feat: elaborate * simp argument
2021-08-15 08:02:21 -07:00
Leonardo de Moura
3c68703f39
feat: elaborate <- modifier at simp arguments
2021-08-15 07:07:58 -07:00
Leonardo de Moura
7c5ab8b4c9
chore: prepare to add <- as simp argument
2021-08-14 06:59:55 -07:00
Leonardo de Moura
25344453c0
feat: add simpStar parser
2021-08-14 06:29:26 -07:00
Leonardo de Moura
cbd36e897b
chore: remove ToExpr Expr
2021-08-14 06:16:46 -07:00
Leonardo de Moura
d8340f55a5
doc: document new binop% elaborator
2021-08-13 20:10:30 -07:00
Leonardo de Moura
d52de3392b
chore: remove workaround
2021-08-13 19:35:47 -07:00
Leonardo de Moura
a15a36b8d3
chore: cleanup Subarray instances
2021-08-13 19:29:09 -07:00
Leonardo de Moura
ddec62f77b
feat: synthesize pending metavariables created before binop% too
...
Reason: some of the `binop%` arguments may be let-variables, and the
values assigned to the let-variables may be in the pending list.
2021-08-13 19:25:45 -07:00
Leonardo de Moura
2994747ed9
chore: remove workaround
2021-08-13 18:25:32 -07:00
Leonardo de Moura
4ee2f80d66
fix: improve binop% elaborator
2021-08-13 17:33:32 -07:00
Leonardo de Moura
4b58c4cc02
refactor: instances that "hide" coercions
...
Example:
```
instance [CoeHTCT α β] [Add β] : HAdd α β β where
hAdd a b := Add.add a b
```
2021-08-13 17:18:55 -07:00
Leonardo de Moura
ef46b0145b
chore: use binop% to define the notations >> and <|>
...
Motivation: we want to delete the instances
```
instance [CoeHTCT α β] [OrElse β] : HOrElse α β β where
hOrElse a b := OrElse.orElse a b
instance [CoeHTCT α β] [OrElse β] : HOrElse β α β where
hOrElse a b := OrElse.orElse a b
instance [CoeHTCT α β] [AndThen β] : HAndThen α β β where
hAndThen a b := AndThen.andThen a b
instance [CoeHTCT α β] [AndThen β] : HAndThen β α β where
hAndThen a b := AndThen.andThen a b
```
after we update stage0
2021-08-13 17:13:01 -07:00
Leonardo de Moura
b012050917
chore: remove some macros that use binop%
...
For example, given `i : Int` and `n : Nat`, we don't want to coerce `n`
into a `Int` in the term `i ^ n`.
2021-08-13 17:00:59 -07:00
Leonardo de Moura
3418eb7e1f
fix: check whether CoeHTCT has already been defined or not at hasCoe
2021-08-13 17:00:59 -07:00
Leonardo de Moura
be23709737
chore: use binop% to define ++ notation
2021-08-13 16:26:35 -07:00
Leonardo de Moura
d3d03df83c
feat: new elaborator for binop%
...
cc @gebner.
2021-08-13 15:44:59 -07:00
Leonardo de Moura
24fe2875c6
chore: change Pow class
...
Based on the suggestion at https://github.com/leanprover/lean4/issues/433
2021-08-12 13:59:55 -07:00
Sebastian Ullrich
16026e9edd
perf: restore monad instance specialization hack
2021-08-12 21:09:09 +02:00
Leonardo de Moura
a6b6d61b39
chore: simplify mkProjStx?
2021-08-12 09:50:43 -07:00
Leonardo de Moura
da03262937
fix: check redundant sources at structure instance notation
2021-08-12 09:16:30 -07:00
Sebastian Ullrich
917eb4d081
chore: collect stdlib compilation flags in new header
2021-08-12 07:51:50 -07:00
Sebastian Ullrich
9c15f94be3
perf: do not use parsers from the current stage inside quotations by default
2021-08-12 07:51:50 -07:00
Sebastian Ullrich
20accf5105
feat: revise macro parameter syntax
2021-08-12 07:48:42 -07:00
Sebastian Ullrich
6c220423ed
chore: adjust stx precedences
2021-08-12 07:48:42 -07:00
Leonardo de Moura
c68882ca67
feat: structure instance notation with multiple sources
...
closes #462
closes #463
2021-08-12 06:18:47 -07:00
Leonardo de Moura
a02a490a10
feat: add mkProjStx?
2021-08-12 05:41:00 -07:00
Leonardo de Moura
2dfde4637f
fix: index out of bounds
2021-08-12 05:39:19 -07:00
Leonardo de Moura
accf198a88
feat: add ExplicitSourceInfo
2021-08-12 04:29:19 -07:00
Leonardo de Moura
c591902547
refactor: add structure to Source.explicit
2021-08-12 04:10:47 -07:00
Leonardo de Moura
45e4dc26e1
refactor: simplify Source.explicit
2021-08-12 03:40:30 -07:00
Daniel Selsam
5952a857cd
feat: pp.analyze improve heuristics for fun binders
2021-08-12 09:37:57 +02:00
Daniel Selsam
638d0ca8ed
feat: pp.instances and pp.instanceTypes
2021-08-12 09:33:30 +02:00
Daniel Selsam
040141f137
feat: unexpander for Subtype
2021-08-12 09:32:33 +02:00
Leonardo de Moura
67103f54a9
chore: add TODOs for multiple sources
2021-08-11 19:28:49 -07:00
Leonardo de Moura
74bd537465
fix: generation of to* field names
2021-08-11 17:25:02 -07:00
Leonardo de Moura
d78101f00d
chore: remove mutual recursion workaround
...
It was a leftover hack for the old frontend.
2021-08-11 16:57:53 -07:00
Leonardo de Moura
4abbb3d74c
chore: cleanup
2021-08-11 16:05:07 -07:00
Leonardo de Moura
f1738ce2a0
feat: add macro for expanding field abbrev notation
...
The new macro allows us to use the field abbrev notation in patterns
too. See new test.
2021-08-11 16:02:50 -07:00
Leonardo de Moura
09c2b668e6
feat: allow multiple sources in the structure instance parser
...
This commit also fixes some macros, and make sure the elaborator still
works, but it does not support multiple sources yet.
2021-08-11 13:07:56 -07:00
