Module Qcert.Translation.Lang.WasmAsttoWasmBinary

Require Import WasmAstRuntime.
Require Import WasmBinaryRuntime.

Section WasmAsttoWasmBinary.
  Section Top.
    Axiom wasm_ast_to_wasm : wasm_ast -> wasm.
  End Top.

End WasmAsttoWasmBinary.

Extract Constant wasm_ast_to_wasm => "Wasm.Encode.encode".