Marcus Rossel
60d056ffdf
doc: fix typos ( #3543 )
...
The doc comment on
[Lean.Meta.viewSubexpr](https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/ExprLens.html#Lean.Meta.viewSubexpr )
also seems broken, but I don't know how to fix it.
2024-02-29 13:23:19 +00:00
Joe Hendrix
710c3ae9e8
chore: upstream exact? and apply? from Std ( #3447 )
...
This is still a draft PR, but includes the core exact? and apply?
tactics.
Still need to convert to builtin syntax and test on Std.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
2024-02-23 21:55:24 +00:00
Henrik Böving
23e49eb519
perf: add prelude to all Lean modules
2024-02-18 14:55:17 -08:00
Leonardo de Moura
457d33d660
feat: configuration options zeta and zetaDelta
...
TODO: bootstrapping issues, set `zetaDelta := false` in the simplifier.
2024-02-18 14:14:55 -08:00
Kyle Miller
433c4d22c2
fix: exposeRelevantUniverses was inserting the whole expression into itself
...
This bug appeared in c9db8619f1
2024-02-17 17:53:19 -08:00
Leonardo de Moura
ef9a6bb839
fix: an equation lemma with autoParam arguments fails to rewrite ( #3316 )
...
closes #2243
2024-02-17 13:42:34 +00:00
Marcus Rossel
509f35df02
doc: fix typos ( #3236 )
2024-02-01 19:03:58 +00:00
Marcus Rossel
12dc171c48
doc: fix typos ( #3178 )
2024-01-14 14:02:51 +00:00
Leonardo de Moura
3a13200772
refactor: add configuration options to control WHNF
...
This commit also removes parameter `simpleReduce` from discrimination
trees, and take WHNF configuration options.
Reason: it is more dynamic now. For example, the simplifier
will be able to use different configurations for discrimination tree insertion
and retrieval. We need this feature to address issues #2669 and #2281
This commit also removes the dead Meta.Config field `zetaNonDep`.
2023-10-25 03:12:35 -07:00
Leonardo de Moura
aecc83e2fc
chore: add some doc strings and cleanup
2023-10-25 03:12:35 -07:00
Leonardo de Moura
b8af36fba0
chore: update comments at src/Lean/Meta/Basic.lean
...
Co-authored-by: Timo <timorcb@gmail.com>
2023-10-14 10:20:29 -07:00
Leonardo de Moura
3bc18797b0
fix: ensure transient cache results for different transparency modes don't mix up
2023-10-14 10:20:29 -07:00
Leonardo de Moura
e3b08060d0
fix: chore add workaround for corrupted cache
2023-10-14 10:20:29 -07:00
Leonardo de Moura
2253b788b4
perf: fine grain isDefEq cache for terms not containing metavariables
2023-10-14 10:20:29 -07:00
int-y1
8d7520b36f
chore: fix typos in comments
2023-10-08 10:46:05 +02:00
Scott Morrison
1dd443a368
doc: improve doc-string for Meta.getConst?
2023-08-24 07:42:28 -07:00
Mario Carneiro
9ec9ea61a4
fix: infinite loop in isClassApp?
2023-05-30 18:47:17 -07:00
Leonardo de Moura
83cc0bcc96
fix: fixes #2199
2023-05-28 18:29:09 -07:00
Gabriel Ebner
d3c55ef249
perf: do not reset tc cache when adding local instances
2023-03-16 15:26:38 -07:00
Gabriel Ebner
a2f5959118
chore: use deriving Nonempty
2022-12-22 03:48:15 +01:00
Gabriel Ebner
eeab2af7ae
fix: remove Inhabited Environment instance
2022-12-21 20:08:08 +01:00
Gabriel Ebner
e386d5941e
refactor: replace ignoreLevelMVarDepth by levelAssignDepth
2022-12-19 20:14:17 +01:00
Sebastian Ullrich
6169435259
refactor: consolidate MessageData constructors into lazy formatting with infos
2022-12-07 19:16:25 +01:00
Gabriel Ebner
75aa732af5
doc: mention ignoreLevelMVarDepth
2022-11-15 11:29:26 -08:00
Leonardo de Moura
1cc58e60ef
fix: fixes #1829
2022-11-15 08:31:36 -08:00
Mario Carneiro
583e023314
chore: snake-case attributes (part 2)
2022-10-19 09:28:08 -07:00
Leonardo de Moura
3f076fc836
perf: missing annotations and helper instances
2022-10-14 08:42:50 -07:00
Gabriel Ebner
ba57ad3480
feat: add implementation-detail hypotheses
2022-10-11 17:24:35 -07:00
Mario Carneiro
85119ba9d1
chore: move Std.* data structures to Lean.*
2022-09-26 05:46:04 -07:00
Ed Ayers
2a6697e077
feat: goal-diffs ( #1610 )
2022-09-24 11:46:11 +02:00
Mario Carneiro
6392c5b456
chore: import reductions
2022-09-15 14:02:38 -07:00
Gabriel Ebner
3a9152f007
chore: improve defeq traces
2022-08-15 08:55:25 -07:00
Leonardo de Moura
52f3a3ff2c
refactor: move mkArrow to CoreM
2022-08-10 20:21:42 -07:00
Leonardo de Moura
18ccc01cf1
feat: add inferType for LCNF
2022-08-09 17:33:24 -07:00
Leonardo de Moura
0156b59ef1
chore: enforce naming convention
2022-08-01 09:58:11 -07:00
Patrick Massot
435017231d
doc: add some docstrings and docstrings details
2022-07-29 10:30:43 -07:00
Leonardo de Moura
6db01d8e48
perf: simpler isDefEq caching
...
We don't try to reuse the cache contents between different `isDefEq`
calls. Thus, we can cache more results and ignore whether the state of
the metavariable context affects them or not.
Closes #1102
2022-07-27 19:35:45 -07:00
Leonardo de Moura
c210781af8
refactor: add doc strings, cleanup, and dotted notation friendly API
...
See #1346
2022-07-27 16:01:15 -07:00
Leonardo de Moura
642b30ab47
feat: add withInstImplicitAsImplict
2022-07-26 12:35:30 -07:00
Leonardo de Moura
3896244c55
chore: cleanup
2022-07-25 22:39:56 -07:00
Leonardo de Moura
90fb110cc9
refactor: improve FVarId method discoverability
...
See issue #1346
2022-07-25 22:18:58 -07:00
Leonardo de Moura
8335a82aed
refactor: improve MVarId method discoverability
...
See issue #1346
2022-07-24 21:36:33 -07:00
Leonardo de Moura
a62949c49b
refactor: add type LevelMVarId (and abbreviation LMarId)
...
Motivation: make sure we do not mixup metavariable ids for
expression and universe level.
cc @bollu
2022-07-24 17:21:45 -07:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! ( #1354 )
2022-07-22 12:05:31 -07:00
Mario Carneiro
f36f94a0e3
fix: malformed/misaligned markdown code fences (part 2)
2022-07-22 13:03:02 +02:00
Leonardo de Moura
da71dd3d77
chore: docstring
2022-07-18 22:16:32 -04:00
Leonardo de Moura
3fd2250799
feat: add higherOrderOutParam to ParamInfo
...
Helper info for #1299
2022-07-11 18:52:01 -07:00
Leonardo de Moura
709f22c8e4
feat: add field dependsOnHigherOrderOutParam to ParamInfo
...
See issue #1299
2022-07-11 17:49:49 -07:00
Gabriel Ebner
a8cab84735
refactor: use computed fields for Expr
2022-07-11 14:19:41 -07:00
Gabriel Ebner
3176943750
refactor: use computed fields for Level
2022-07-11 14:19:41 -07:00
