lean4-htt/tests/lean/autoPPExplicit.lean.expected.out at 5b2e39e3b5d93a099caa3530216f2033343b9dcd - max/lean4-htt - maxgit: wireguard access, git repository.

max/lean4-htt

Markus Himmel eda467e066

fix: typo in application type mismatch error message (#8290 )

This PR fixes a typo that was introduced recently.

2025-05-12 13:35:29 +00:00

8 lines

204 B

Text

Raw Blame History

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

 autoPPExplicit.lean:2:26-2:31: error: Application type mismatch: In the application
   @Eq.trans α a (b = c)
 the final argument
   b = c
 has type
   Prop : Type
 but is expected to have type
   α : Sort u_1