Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/floatbits
/
.
/
tests
/
lean
/
metaEvalInstMessage.lean
blob: 43db5a58e9161eb3fce0667351ab468deea4ba28 [
file
] [
edit
]
import
Lean
def
double
(
x
:
Nat
)
:=
2
*
x
#eval double