-
Notifications
You must be signed in to change notification settings - Fork 251
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.
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
[Merged by Bors] - feat: port pi_fin.reflect
instance
#3430
Conversation
88add10
to
2f9f625
Compare
This PR/issue depends on:
|
@eric-wieser I've pushed a commit that makes it as it gets right now. |
…to eric-wieser/port-Fin.reflect
let x : Fin 0 → ℕ := ![] | ||
let .true ← isDefEq (toExpr x) q((![] : Fin 0 → ℕ)) | failure | ||
|
||
#eval do |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is there a better pattern than #eval do
here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would like to define #assert
(which can run MetaM code), but haven't done so yet. AFAIK this is as good as it gets for now.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
By the way, isDefEq
doesn't do typechecking, so it might be good to do typechecks for toExpr
and toTypeExpr
. See https://github.com/leanprover-community/mathlib4/blob/master/test/DeriveToExpr.lean
bors merge |
This was skipped during the initial port of this file. There are some golfing discussions [here on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/unquoteExpr.3A.20inst.E2.9C.9D.C2.B2.2E2.20.3A.20Expr/near/349273797) that we could revisit later Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Pull request successfully merged into master. Build succeeded: |
pi_fin.reflect
instancepi_fin.reflect
instance
This was skipped during the initial port of this file. There are some golfing discussions [here on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/unquoteExpr.3A.20inst.E2.9C.9D.C2.B2.2E2.20.3A.20Expr/near/349273797) that we could revisit later Co-authored-by: Gabriel Ebner <gebner@gebner.org>
This was skipped during the initial port of this file.
There are some golfing discussions here on Zulip that we could revisit later
ToExpr
deriving handler #3215