Mercurial > hg > Papers > 2023 > soto-master
view Paper/src/escape_agda.rb @ 3:c28e8156a37b
Add paper init~agda
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 20 Jan 2023 13:40:03 +0900 |
parents | a72446879486 |
children | d4f3d9d283a2 |
line wrap: on
line source
#!/usr/bin/env ruby Suffix = '.agda.replaced' EscapeChar = '!' FileName = ARGV.first ReplaceTable = { '→' => 'rightarrow', '⊔' => 'sqcup', '∷' => 'text{::}', '∙' => 'circ', '≡' => 'equiv', '×' => 'times', '⟨' => 'langle', '⟩' => 'rangle', '₁' => 'text{1}', '₂' => 'text{2}', '₃' => 'text{3}', 'ℕ' => 'mathbb{N}', '∎' => 'blacksquare', 'λ' => 'lambda', '∧' => 'wedge', '⇒' => 'Rightarrow', '¬' => 'neg', '≤' => 'leq', '⊥' => 'bot', "'" => "prime", '⊤' => 'top' } code = File.read(FileName) ReplaceTable.each do |k, v| escaped_str = EscapeChar + "$\\#{v}$" + EscapeChar code = code.gsub(k, escaped_str) end File.write(FileName.sub(/.agda$/, Suffix), code)