Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Avoid deprecated getMVarDecl etc. #68

Closed
JLimperg opened this issue Jul 26, 2022 · 0 comments · Fixed by #77
Closed

Avoid deprecated getMVarDecl etc. #68

JLimperg opened this issue Jul 26, 2022 · 0 comments · Fixed by #77

Comments

@JLimperg
Copy link
Contributor

Many basic functions have changed recently, e.g. getMVarDecl to MVarId.getDecl. The old versions are deprecated, so we (I) should update the book accordingly. See leanprover/lean4#1346.
JLimperg added a commit to JLimperg/lean4-metaprogramming-book that referenced this issue Oct 26, 2022
@JLimperg
metam: various improvements
3598e20 
* Use `Lean.MVarId.withContext` instead of the deprecated
  `withMVarContext`, and the same for other such functions.
* Use `.const` instead of `mkConst`, and the same for other `Expr`
  constructors.
* Use `isImplementationDetail` instead of `isAuxDecl`.
* Fix an error in the WHNF section. (Thanks to Jasmin Blanchette.)
* Fix a confusing part of the transparency section. (Thanks to Jasmin
  Blanchette.)
* Various small improvements.

fixes leanprover-community#76
partially addresses leanprover-community#68
JLimperg added a commit to JLimperg/lean4-metaprogramming-book that referenced this issue Oct 26, 2022
@JLimperg
cheat-sheet,intro: avoid deprecated functions
da7d380 
fixes leanprover-community#68
@JLimperg JLimperg mentioned this issue Oct 26, 2022
Merged
arthurpaulino pushed a commit that referenced this issue Oct 26, 2022
@JLimperg
Clean up some deprecations etc. (#77)
761cfb3 
* Update Lean to nightly-2022-10-24

Notable changes:

- Lake's module discovery has apparently changed, so we now need to
  specify directory globs for `main` and `extra`.
- Attributes now use snake_case instead of camelCase.

* metam: various improvements

* Use `Lean.MVarId.withContext` instead of the deprecated
  `withMVarContext`, and the same for other such functions.
* Use `.const` instead of `mkConst`, and the same for other `Expr`
  constructors.
* Use `isImplementationDetail` instead of `isAuxDecl`.
* Fix an error in the WHNF section. (Thanks to Jasmin Blanchette.)
* Fix a confusing part of the transparency section. (Thanks to Jasmin
  Blanchette.)
* Various small improvements.

fixes #76
partially addresses #68

* expressions: `mkConst` => `Expr.const` etc.

Also minor formulation improvements.

* expressions: correct spelling of "de Bruijn"

* dsls,elaboration: `mkConst` => `Expr.const` etc.

* cheat-sheet,intro: avoid deprecated functions

fixes #68
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Clean up some deprecations etc. JLimperg/lean4-metaprogramming-book
1 participant
@JLimperg