comparison paper/escape_agda.rb @ 59:5450e7ae5fa5

Mini fixes
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 01 Feb 2017 15:27:15 +0900
parents fb42478e4c96
children 40ae32725e55
comparison
equal deleted inserted replaced
58:68bf744d726e 59:5450e7ae5fa5
4 EscapeChar = '@' 4 EscapeChar = '@'
5 FileName = ARGV.first 5 FileName = ARGV.first
6 6
7 ReplaceTable = { 7 ReplaceTable = {
8 '->' => 'rightarrow', 8 '->' => 'rightarrow',
9 '⊔' => 'sqcup',
9 '∷' => 'text{::}', 10 '∷' => 'text{::}',
10 '∙' => 'circ', 11 '∙' => 'circ',
11 '≡' => 'equiv', 12 '≡' => 'equiv',
12 '×' => 'times', 13 '×' => 'times',
13 '⟨' => 'langle', 14 '⟨' => 'langle',