Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/floatbits
/
.
/
tests
/
playground
/
ir.lean
blob: 8514077524471b6a7e0eedc0134349e72ca0997a [
file
] [
edit
]
import
init
.
lean
.
compiler
.
ir
open
Lean
.
IR
def
tst1
:
IO
Unit
:=
let
fbody
:
FnBody
:=
FnBody
.
vdecl
`x IRType.uint32 (Expr.lit (LitVal.num 0)) $
FnBody.ret `
x
;
IO
.
println $ format fbody
def
main
:
IO
Unit
:=
tst1