Yuichi Nishiwaki
Yuichi Nishiwaki
The Satysfi language allows explicit type annotation at let binding with no function arguments like the following: ``` let foo : int = `hello` in ... ``` However, currently, it...
Given the following code ``` type 'a id = 'a module Foo : sig val my-id: ('a -> 'a) id end = struct let my-id a = a end Foo.my-id...
I added five math char classes - sans serif - bold serif - italic sans serif - bold italic sans serif - typewriter and three math font selectors - `\mathit`...
Although this may be not a bug but a matter of preference, (big) curly braces in math mode are drawn a little strangely. I like upper and lower parts to...
Tab characters in `\d-code` block are not displayed correctly. For the following code, ``` @require: stdjareport @require: code document (| title = {\SATySFi;}; author = {Nanashi Taro}; |) '< %...
Currently satysfi only supports a subset of font styles defined in unicode to be used in math expressions [2]. In [1] many (maybe all?) font styles available in unicode are...
pdfs generated by satysfi contain no '/ToUnicode CMap' info for parentheses in math expressions, mainly because satysfi draws parentheses using graphics instead of placing characters. This breaks copy&pasting from such...
To display the following program, ```Lean inductive perm | trans aaaaaa aaaaa : Π {l₁ l₂ l₃ : list α}, perm l₁ l₂ → perm l₂ l₃ → perm l₁...
Satysfi does not support for combining diacritical mark for kana (仮名) characters. For some reasons, macOS often tries to decompose unicode characters into a sequence of combining diacritical marks. In...
Given a source code like the following: ``` (ややこしいので，実装に用いる定理証明支援系を\dfn{メタ言語}，これから実装される言語を\dfn{オブジェクト言語}と呼びます．) \listing{ * パーサー: DSL * 束縛関係の管理, 型検査, 型推論: 高階抽象構文(HOAS) * 効率的な評価器: Normalization by Evaluation * タクティック言語: メタ言語のタクティック言語 }% } +p{ 具体的な方針は以下の通りです．...