blob: 95d34b152a0ac8f74dc981eb9edf95a33df3ab5b [file] [edit]
389.lean:7:14-7:17: error: application type mismatch
getFoo bar
argument
bar
has type
Bar Nat : Type
but is expected to have type
Foo ?m : Type
getFoo bar.toFoo : Nat