SATySFi
SATySFi copied to clipboard
gfngfn
A statically-typed, functional typesetting system
As written in a comment in `typeenv.ml`, SATySFi does not check whether a type constructor has the same arity in the structure and the signature: https://github.com/gfngfn/SATySFi/blob/69e62f66056b5644461f73c5fe841003602b0938/src/frontend/typeenv.ml#L1221 For example, SATySFi does...
in `${}`, `\partial` generates non-italic image of `∂` , which doesn't align well with successors.
Tab characters in `\d-code` block are not displayed correctly. For the following code, ``` @require: stdjareport @require: code document (| title = {\SATySFi;}; author = {Nanashi Taro}; |) '< %...
SATySFi request the document type with the `-t` option and `--type-check-only` option. # Bug example input (file name is `test.saty`) ``` 42 ``` output ``` $ satysfi -t test.saty ----...
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₁...
In function arguments, we can use `let`, `let-rec`, and `let-math`. However, we cannot use `let-inline` or `let-block` (syntax error at parser). Is this a design choice of SATySFi, or a...
I noticed that optional arguments are sometimes not supported (syntax error). Example: ```satysfi % These are good. let f ?:x y = () let-inline ctx \f ?:x y = read-inline...
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...