#assertType 5 : ?_ does in fact result in success - Githubissues

leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/

Apache License 2.0

204 stars 47 forks source link

#assertType 5 : ?_ does in fact result in success #101

Closed jcommelin closed 10 months ago

jcommelin commented 1 year ago

https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/4fc5d4144efd48ec0c30a2b5f726a2055da46448/lean/main/intro.lean#L148 contains

Without that line, #assertType 5 : ?_ would result in success.

But when I test this, I do get success. Maybe #assertType [] : ?_ is a better example?