Something went wrong. Try again.
Verified branch relaxing assembler in Isabelle/HOL with provably minimal bytecode layouts
Something went wrong. Try again.
123456789101112theory Export imports Frontendbegin
definition ascii :: "integer \<Rightarrow> char" where "ascii = char_of"
definition ordinal :: "char \<Rightarrow> integer" where "ordinal = of_char"
export_code process binary artifact disassemble ascii ordinal in SML module_name Span file_prefix span
end