lean4-htt

Author SHA1 Message Date

Author	SHA1	Message	Date
Kyle Miller	044bfdb098	feat: eliminate `letFun` support, deprecate `let_fun` syntax (#9086 ) This PR deprecates `let_fun` syntax in favor of `have` and removes `letFun` support from WHNF and `simp`.	2025-06-30 02:10:18 +00:00
Kyle Miller	31981090e4	feat: make `intro` be aware of `let_fun` (#3115 ) Adds support for `let_fun` to the `intro` and `intros` tactics. Also adds support to `intro` for anonymous binder names, since the default variable name for a `letFun` with an eta reduced body is anonymous.	2024-01-31 08:55:52 +00:00

Kyle Miller

044bfdb098

feat: eliminate letFun support, deprecate let_fun syntax (#9086 )

This PR deprecates `let_fun` syntax in favor of `have` and removes
`letFun` support from WHNF and `simp`.

2025-06-30 02:10:18 +00:00

Kyle Miller

31981090e4

feat: make intro be aware of let_fun (#3115 )

Adds support for `let_fun` to the `intro` and `intros` tactics. Also
adds support to `intro` for anonymous binder names, since the default
variable name for a `letFun` with an eta reduced body is anonymous.

2024-01-31 08:55:52 +00:00

2 commits