Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/setConfig
/
.
/
tests
/
lean
/
modBug.lean.expected.out
blob: 9bee5bd5bb31df688f32f5f0ec943c2ee979f3b3 [
file
] [
edit
]
modBug
.
lean
:
1
:
48
-
1
:
64
:
error
:
application type mismatch
Nat
.
zero_ne_one
(
Nat
.
mod_zero
1
)
argument
Nat
.
mod_zero
1
has type
1
%
0
=
1
:
Prop
but
is
expected to have type
0
=
1
:
Prop