packagetype _plain packagetype _code primitive !if val code -> void primitive !goto lab -> void package main _plain kind K_number int32 kind K_func function K_number -> K_number package R_101_B _code local (/main/K_number) x __argument code .begin inv !if val (/main/K_number) 1 code inv !goto lab .begin constant (K_func) R_101 = R_101_B