Leonardo de Moura
ab162b3f52
fix: isDefEq, whnf, simp caching and configuration ( #6053 )
...
This PR fixes the caching infrastructure for `whnf` and `isDefEq`,
ensuring the cache accounts for all relevant configuration flags. It
also cleans up the `WHNF.lean` module and improves the configuration of
`whnf`.
2024-11-18 01:17:26 +00:00
Joachim Breitner
d4fdb5d7c0
fix: getFunInfo, inferType to use withAtLeastTransparency, not withTransparency ( #5563 )
...
when the transparency mode is `.all`, then one expects `getFunInfo` and
`inferType` to also work with that transparency mode.
Fixes #5562
Fixes #2975
Fixes #2194
2024-10-04 13:04:35 +00:00
Joachim Breitner
60096e7d15
refactor: more idiomatic syntax for if h: ( #5567 )
...
https://github.com/leanprover/lean4/pull/5552 introduced a fair number
of `if h:`, but the slightly preferred style is `if h :`, with a space,
so here goes a quick `sed`.
2024-10-01 15:23:54 +00:00
TomasPuverle
ddec5336e5
chore: switch obvious cases of array "bang"[]! indexing to rely on hypothesis ( #5552 )
...
Update certain uses of `arr[i]!` to use the "provably correct" version
`arr[i]`, in order to use "best practices".
Some motivation and discussion on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.20compiler.2Felaborator.20development.20question/near/472934715 )
2024-10-01 11:12:22 +00:00
Henrik Böving
23e49eb519
perf: add prelude to all Lean modules
2024-02-18 14:55:17 -08: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
Leonardo de Moura
0c5dfd78d7
chore: style
2022-07-10 15:26:26 -07:00
Leonardo de Moura
2ebcf29cde
chore: use a[i]! for array accesses that may panic
2022-07-02 15:12:05 -07:00
Leonardo de Moura
a028a69159
feat: cache isProp and isDecInst at FunInfo
2022-02-04 17:57:28 -08:00
Leonardo de Moura
736f119beb
feat: add FunInfo.getArity
2021-09-14 15:58:00 -07:00
Leonardo de Moura
d1d7ce1839
feat: start support for strict implicit binder annotation
2021-08-03 18:42:15 -07:00
Leonardo de Moura
8b4cdcfddd
chore: fix mutable variable shadowing
2021-05-22 19:24:41 -07:00
Leonardo de Moura
3388c63e11
fix: typo at ParamInfo.isExplicit
2021-01-11 07:08:17 -08:00
Leonardo de Moura
01b6f4f06b
fix: incorrect shadowing of let mut variable
2020-12-28 15:52:11 -08:00
Leonardo de Moura
2d2d39c78e
chore: use mut
2020-11-07 17:32:13 -08:00
Leonardo de Moura
5ea49c92bb
chore: cleanup
2020-10-27 13:26:21 -07:00
Leonardo de Moura
13c2a8ff51
chore: remove #lang lean4 header
2020-10-25 09:54:07 -07:00
Leonardo de Moura
c3897fff31
chore: move to new frontend
2020-10-19 12:15:48 -07:00
Leonardo de Moura
98f7e9b3e4
chore: naming convention
2020-09-24 19:22:24 -07:00
Leonardo de Moura
249bda16c0
chore: remove prelude commands from Lean package
2020-06-25 11:21:17 -07:00
Leonardo de Moura
4ccc3fef52
chore: move Init.Lean files to Lean package
2020-05-26 15:04:35 -07:00
