search

leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
204 stars 47 forks source link

fix(intro): fix counterexample #102

Closed jcommelin closed 10 months ago

jcommelin commented 1 year ago

#assertType 5 : ?_ actually succeeds, because the default type of 5 is Nat. By changing the counterexample to #assertType [] : ?_ we get the expected failure.

closes #101

Julian commented 10 months ago

(Looks good to me after confirming what's here indeed succeeds without that line and fails with the suggested replacement example.)