Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/floatbits
/
.
/
tests
/
lean
/
973b.lean.expected.out
blob: 0cd8213d49b1ffc90092eeb1bdd96f62f2e0b2c5 [
file
] [
edit
]
973b
.
lean
:
5
:
8
-
5
:
10
:
warning
:
declaration uses
'sorry'
973b
.
lean
:
9
:
8
-
9
:
11
:
warning
:
declaration uses
'sorry'
[
Meta
.
Tactic
.
simp
.
discharge
]
ex discharge
❌️
?
p x
[
Meta
.
Tactic
.
simp
.
discharge
]
ex discharge
❌️
?
p
(
f x
)