~james/remy

4
e43395488ea9ada734e845de1d029e87990e690f
main
remy/src/Export.thy -rw-r--r--302 bytes ViewLogBlameView rawPermalink 75a5217580 feat(frontend): parameterise checked compiler resource limits 1 months 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 configured artifact vectors reference ascii ordinal in SML module_name Remy file_prefix remy

end