diff --git a/examples/algebra.pg b/examples/algebra.pg index 7073ebb..5938548 100644 --- a/examples/algebra.pg +++ b/examples/algebra.pg @@ -48,7 +48,8 @@ def id_r_op : forall (a : G), a *> e = a := id_lG; def left_id_unique (a : G) (H : forall (b : G), a * b = b) : a = e := eq_trans G a (a * e) e (eq_sym G (a * e) a (id_rG a)) (H e); -def right_id_unique (a : G) (H : forall (b : G), b * a = b) : a = e := #left_id_unique G (*>) e id_lG a H; +def right_id_unique (a : G) (H : forall (b : G), b * a = b) : a = e := + #left_id_unique G (*>) e id_lG a H; section Group diff --git a/examples/sets.pg b/examples/sets.pg new file mode 100644 index 0000000..d71f92f --- /dev/null +++ b/examples/sets.pg @@ -0,0 +1,2 @@ +axiom set : ★; +axiom ∈ : set → set → ★; diff --git a/lib/Expr.hs b/lib/Expr.hs index 2bb721b..6037388 100644 --- a/lib/Expr.hs +++ b/lib/Expr.hs @@ -183,8 +183,8 @@ prettyExpr k expr = case expr of | otherwise -> piType where (top :| rest) = collectArrows expr - piType = group $ hang 4 $ prettyExpr 3 top <+> align (sep $ map (("->" <+>) . prettyExpr 2) rest) - Pi{} -> group $ hang 4 $ "∏" <+> align (sep grouped) <> "," <> line <> align (prettyExpr 0 body) + piType = group $ hang 4 $ prettyExpr 3 top <+> align (sep $ map (("→" <+>) . prettyExpr 2) rest) + Pi{} -> group $ hang 4 $ "forall" <+> align (sep grouped) <> "," <> line <> align (prettyExpr 0 body) where (params, body) = collectPis expr grouped = pretty <$> groupParams params @@ -195,7 +195,7 @@ prettyExpr k expr = case expr of where (params, body) = collectLambdas expr grouped = pretty <$> groupParams params - lambdaForm = group $ hang 4 $ "λ" <+> align (sep grouped) <+> "=>" <> line <> align (prettyExpr 0 body) + lambdaForm = group $ hang 4 $ "λ" <+> align (sep grouped) <+> "⇒" <> line <> align (prettyExpr 0 body) Let{} -> group $ vsep diff --git a/lib/Parser.hs b/lib/Parser.hs index 1f2cd29..fcd6092 100644 --- a/lib/Parser.hs +++ b/lib/Parser.hs @@ -46,7 +46,7 @@ symbol :: Text -> Parser () symbol = void . L.symbol skipSpace symbols :: String -symbols = "!@#$%^&*-+=<>,./?[]{}\\|`~'\"∧∨⊙×≅" +symbols = "!@#$%^&*-+=<>,./?[]{}\\|`~'\"∧∨⊙×≅∈⊆⊂⊃⊇" pKeyword :: Text -> Parser () pKeyword keyword = void $ lexeme (string keyword <* notFollowedBy alphaNumChar)