~james/remy

remy/src/Export.thy -rw-r--r-- 359 bytes
2d73ca56 — james chore(import): snapshot james.dad.town/remy at 76b7f307a15a 15 hours ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
theory Export
  imports Examples Delivery
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 delivery ascii ordinal in SML module_name Remy file_prefix remy

end