lean4-htt/tests/ir/tst1.ir

19 lines
No EOL
375 B
Text

[lean_dbg_print_str] external print_str (s : object)
[lean_dbg_print_num] external print_num (s : object)
defconst x : object :=
main:
y : uint32 := 10;
z : uint32 := 20;
r : uint32 := add y z;
r' : object := box r;
ret r';
def main : int32 :=
entry:
s : object := "hello world";
call print_str s;
v := call x;
call print_num v;
c : int32 := 0;
ret c;