~james/span

span/src/Export.thy -rw-r--r-- 300 bytes
0c6f163a — james chore(import): snapshot james.dad.town/span at 868a68649c22 14 hours ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
theory Export
  imports Frontend
begin

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