~james/remy

31d281ada88d2822fbbece49ea5e511b0ad3ada3
main
remy/src/Export.thy -rw-r--r--323 bytes ViewLogBlameView rawPermalink 31d281ada8 feat(checker): validate native stack and register effects 23 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 vectors reference ascii ordinal in SML module_name Remy file_prefix remy

end