~james/remy

4
7cb596d931d773db10cc8df8c329cd8b881a8826
main
remy/src/Export.thy -rw-r--r--341 bytes ViewLogBlameView rawPermalink 7cb596d931 feat(x86): prove emitted instruction execution and return-frame consumption 13 days ago
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
theory Export
  imports Examples
begin

definition ascii :: "integer \<Rightarrow> char" where "ascii = char_of"

definition ordinal :: "char \<Rightarrow> integer" where "ordinal = of_char"

export_code validate disassemble configured artifact baseline vectors reference simulate ascii ordinal in SML module_name Remy file_prefix remy

end