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

metam: use isImplementationDetail instead of isAuxDecl #76

Closed
JLimperg opened this issue Oct 20, 2022 · 0 comments · Fixed by #77
Closed

metam: use isImplementationDetail instead of isAuxDecl #76

JLimperg opened this issue Oct 20, 2022 · 0 comments · Fixed by #77

Comments

@JLimperg
Copy link
Contributor

(Note to self:) when we iterate over a local context, it does not suffice any more to exclude hypotheses for which isAuxDecl is true; we have to check isImplementationDetail.
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 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