rocq/theories/HiCode.v
The checked module nanofil -O makes of tests/c/prog/hi.c, as a term. Generated by rocq/gallina.pl; rocq/programs.sh checks it is current. Do not edit.
From Stdlib Require Import String ZArith List Ascii
From Nanofil Require Import Term
Import ListNotations
Open Scope string_scope
Open Scope Z_scope
The one-character atom with code n.
The module term.
TApp"module" TListTApp"func" TAtom"main"; TAtom"export"; TAtom"w"; TList[ ]; TListTApp"block" TAtom"start"; TList[ ]; TListTApp"let" TApp"tmp" TAtom"v0"; TAtom"p"; TAtom"copy"; TListTApp"global" TAtom"str.10"; TApp"call" TApp"result" TApp"tmp" TAtom"v1"; TAtom"w"; TApp"global" TAtom"puts"; TListTApp"arg" TAtom"p"; TApp"tmp" TAtom"v0"; TApp"ret" TApp"const" TInt0; TApp"data" TAtom"str.10"; TApp"ro" TAtom"local"; TInt1; TListTApp"item" TAtom"b"; TApp"const" TInt104; TApp"item" TAtom"b"; TApp"const" TInt101; TApp"item" TAtom"b"; TApp"const" TInt108; TApp"item" TAtom"b"; TApp"const" TInt108; TApp"item" TAtom"b"; TApp"const" TInt111; TApp"item" TAtom"b"; TApp"const" TInt0