wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

more symbols + tweaked printed output

Browse source
This commit is contained in:
William Ball 2026-01-22 13:19:41 -05:00
parent 781dba167a
commit fe79ca65c1
Signed by: wball
SSH key fingerprint: SHA256:3K3IvjUp1U5HwsIRYy/vosnG8l/A84LPUSAKQ6oCGKI
4 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
examples/algebra.pg
View file

@ -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 := 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); 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 section Group

2
examples/sets.pg Normal file
View file

@ -0,0 +1,2 @@
axiom set : ★;
axiom ∈ : set → set → ★;

6
lib/Expr.hs
View file

@ -183,8 +183,8 @@ prettyExpr k expr = case expr of
| otherwise -> piType | otherwise -> piType
where where
(top :| rest) = collectArrows expr (top :| rest) = collectArrows expr
piType = group $ hang 4 $ prettyExpr 3 top <+> align (sep $ map (("->" <+>) . prettyExpr 2) rest) 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) Pi{} -> group $ hang 4 $ "forall" <+> align (sep grouped) <> "," <> line <> align (prettyExpr 0 body)
where where
(params, body) = collectPis expr (params, body) = collectPis expr
grouped = pretty <$> groupParams params grouped = pretty <$> groupParams params
@ -195,7 +195,7 @@ prettyExpr k expr = case expr of
where where
(params, body) = collectLambdas expr (params, body) = collectLambdas expr
grouped = pretty <$> groupParams params 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{} -> Let{} ->
group $ group $
vsep vsep

2
lib/Parser.hs
View file

@ -46,7 +46,7 @@ symbol :: Text -> Parser ()
symbol = void . L.symbol skipSpace symbol = void . L.symbol skipSpace
symbols :: String symbols :: String
symbols = "!@#$%^&*-+=<>,./?[]{}\\|`~'\"∧∨⊙×≅" symbols = "!@#$%^&*-+=<>,./?[]{}\\|`~'\"∧∨⊙×≅∈⊆⊂⊃⊇"
pKeyword :: Text -> Parser () pKeyword :: Text -> Parser ()
pKeyword keyword = void $ lexeme (string keyword <* notFollowedBy alphaNumChar) pKeyword keyword = void $ lexeme (string keyword <* notFollowedBy alphaNumChar)