Expected features: - Use unicode characters (lambdas, forall, arrows, etc) (Flag?). - Non dependent products should be printed as arrow types. - Print parenthesis only when needed. - "Uncurryficate" lambdas and products (Flag?): ``` fun (x : A). fun (y : A). fun (z : B). x # should be printed as fun (x y : A) (z : B). x ``` - Separate big outputs into multiple lines in a sensible manner.
Expected features: