Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/floatbits
/
.
/
tests
/
lean
/
failTac.lean.expected.out
blob: 72b99491b682d88ad2090cf067892325d6350ba8 [
file
] [
edit
]
failTac
.
lean
:
2
:
2
-
2
:
6
:
error
:
tactic
'fail'
failed
a b
:
Nat
⊢
False
failTac
.
lean
:
5
:
2
-
5
:
18
:
error
:
giving up
a b
:
Nat
⊢
False
failTac
.
lean
:
14
:
2
-
14
:
21
:
error
:
failing here
case
left
a b
:
Nat
⊢
True
case
right
a b
:
Nat
⊢
False