Dear All,
I am currently working on support for input and output using Unicode into
ProofPower. I would appreciate any feedback on the translation scheme I am
proposing to use, which is described here:
http://www.lemma-one.com/ProofPower/unicode/pp-unicode.html
I am particularly interested to know how good the coverage for the Unicode
characters needed is on different systems and on different applications. You
can see how good your web browser is just by looking at the above Web page,
which includes GIFs that show how LaTeX renders the ProofPower symbols
alongside the Unicode translation as rendered by your browser. To see how good
your mail client is, the following should look something like the HOL
definition of distributed union:
⌜∀ x a⦁ x ∈ ⋃ a ⇔ (∃ s⦁ x ∈ s ∧ s ∈ a)⌝
(There is a complete list of the symbols used at the end of this e-mail.)
Current indications are that Mac OS can do everything that is required, but
that recent Linux systems and MS Windows tend to miss one or two glyphs: the
squared upper case letters I am using for some of the quotation symbols seem to
be poorly supported, for example. Most text editors and word processors on the
systems I have tried do support UTF-8. If anyone can advise on how to extend
the range of Unicode glyphs available on Linux or on how to get font
substitution working nicely with OpenMotif, I would be very grateful.
There is a prototype implementation of the translation as two free-standing
programs pputf8 and utf8pp here:
https://github.com/RobArthan/pp-contrib
(These have been around for a while, but I have just changed them to implement
the somewhat simplified and extended scheme described in the Web page cited
above.)
My immediate plan is to integrate the translation into ProofPower itself, so
that Unicode input and output are options you can select with set_flag (similar
to the way that you can currently select ASCII output, by calling
set_flag(“use_extended_chars”, false)). I will provide separate flags for input
and output.
Below, as a further test of your e-mail client, you will find the ASCII
encoding and UTF-8 encoding of the corresponding Unicode for all the characters
in the ProofPower extended character set.
Regards,
Rob.
%rsub%: ⩥
%bagunion%: ⨄
%bbU%: 𝕌
%Delta%: Δ
%fcomp%: ∘
%Phi%: Φ
%Gamma%: Γ
%down%: ⋎
%Theta%: Θ
%dcat%: ⁀/
%Lambda%: Λ
%mem%: ∈
%notmem%: ∉
%bij%: ⤖
%Pi%: Π
%SML%: 🄼
%rres%: ▷
%Sigma%: Σ
%<:%: 🅃
%Upsilon%: Υ
%boolean%: 𝔹
%Omega%: Ω
%Xi%: Ξ
%Psi%: Ψ
%emptyset%: ∅
%up%: ⋏
%BHH%: ═
%finj%: ⤕
%ffun%: ⇻
%psubset%: ⊂
%intersect%: ∩
%rseq%: 〉
%symdiff%: ⊖
%equiv%: ⇔
%dintersect%: ⋂
%def%: ≜
%lseq%: 〈
%lrelimg%: ⦇
%rrelimg%: ⦈
%rel%: ↔
%overwrite%: ⊕
%<%: ⌜
%fun%: →
%>%: ⌝
%real%: ℝ
%EFT%: █
%and%: ∧
%or%: ∨
%not%: ¬
%implies%: ⇒
%forall%: ∀
%exists%: ∃
%spot%: ⦁
%x%: ×
%SFT%: Ⓢ
%bigcolon%: ⦂
%rcomp%: ⨾
%leq%: ≤
%neq%: ≠
%geq%: ≥
%symbol%: 𝕊
%union%: ∪
%alpha%: α
%beta%: β
%delta%: δ
%select%: ϵ
%phi%: ϕ
%gamma%: γ
%eta%: η
%iota%: ι
%theta%: θ
%kappa%: κ
%fn%: λ
%mu%: μ
%nu%: ν
%psurj%: ⤀
%pi%: π
%chi%: χ
%rho%: ρ
%sigma%: σ
%tau%: τ
%upsilon%: υ
%complex%: ℂ
%omega%: ω
%xi%: ξ
%psi%: φ
%zeta%: ζ
%SX%: ⦏
%BV%: │
%EX%: ⦎
%dunion%: ⋃
%pfun%: ⇸
%inj%: ↣
%dsub%: ⩤
%bottom%: ⊥
%Leftarrow%: ⇐
%psupset%: ⊃
%supset%: ⊇
%fset%: 𝔽
%uptext%: ↗
%dntext%: ↘
%cantext%: ↕
%cat%: ⁀
%extract%: ↿
%map%: ↦
%nat%: ℕ
%surj%: ↠
%pset%: ℙ
%dres%: ◁
%rat%: ℚ
%thm%: ⊢
%ulbegin%: ₍
%ulend%: ₎
%BT%: ├
%uminus%: ﹣
%filter%: ↾
%int%: ℤ
%lbag%: ⟦
%BH%: ─
%rbag%: ⟧
%pinj%: ⤔
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
