Documentation
Batteries
.
Util
.
Panic
Search
Google site search
return to top
source
Imports
Init
Imported by
Batteries
.
panicWith
Batteries
.
panicWith_eq
source
def
Batteries
.
panicWith
{α :
Type
u_1}
(v :
α
)
(msg :
String
)
:
α
Panic with a specific default value
v
.
Equations
Batteries.panicWith
v
msg
=
panic
msg
Instances For
source
@[simp]
theorem
Batteries
.
panicWith_eq
{α :
Type
u_1}
(v :
α
)
(msg :
String
)
:
Batteries.panicWith
v
msg
=
v