diff Paper/escape_agda.rb @ 5:339fb67b4375

INIT rbt.agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 07 Nov 2021 00:51:16 +0900
parents 9176dff8f38a
children
line wrap: on
line diff
--- a/Paper/escape_agda.rb	Sat Nov 06 20:06:24 2021 +0900
+++ b/Paper/escape_agda.rb	Sun Nov 07 00:51:16 2021 +0900
@@ -2,7 +2,7 @@
 # coding: utf-8
 
 Suffix     = '.agda.replaced'
-EscapeChar = '@'
+EscapeChar = '!'
 FileName   = ARGV.first
 
 ReplaceTable = {
@@ -18,6 +18,7 @@
   'ℕ' => 'mathbb{N}',
   '₁' => '_{1}',
   '₂' => '_{2}',
+  '₃' => '_{3}',
   '∎'  => 'blacksquare',
   'λ' => 'lambda',
   '∧' => 'wedge',
@@ -29,7 +30,8 @@
   '∀' => 'forall',
   '#' => '\#',
   '⊤' => '\top',
-  '\'' => '\prime'
+  '\'' => '\prime',
+  '≈' =>  '\approx'
 }
 
 code = File.read(FileName)