From 9cdcc0e79a87186d4dc0c1f46ca3e7f723d0d1c6 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 5 Jun 2024 14:23:45 +0200
Subject: Update Megalodon.hs

---
 source/Megalodon.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/source/Megalodon.hs b/source/Megalodon.hs
index 37479b2..7e75e6d 100644
--- a/source/Megalodon.hs
+++ b/source/Megalodon.hs
@@ -21,7 +21,7 @@ closure :: [ExprOf VarSymbol] -> ExprOf VarSymbol -> Formula
 closure asms stmt = contraction (forallClosure mempty (makeConjunction asms `Implies` stmt))
 
 unAsm :: Asm -> Formula
-unAsm (Asm phi )= phi
+unAsm (Asm phi) = phi
 unAsm (AsmStruct x sp) = TermSymbol (SymbolPredicate (PredicateNounStruct sp)) [TermVar x]
 
 buildBlocks :: Lexicon -> [Block] -> Builder
-- 
cgit v1.2.3


From 3a1c6df56dd7b38c42caf7833025f3830a656aa1 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Mon, 10 Jun 2024 23:50:39 +0200
Subject: Dedupe helper function

---
 source/Syntax/Concrete.hs | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index bad9635..b51b738 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -241,7 +241,7 @@ grammar lexicon@Lexicon{..} = mdo
     asmLetStruct    <- rule $ AsmLetStruct <$> (_let *> var <* _be <* _an) <*> structNounNameless
     asmLet          <- rule $ asmLetNoun <|> asmLetNouns <|> asmLetIn <|> asmLetEq <|> asmLetThe <|> asmLetStruct
     asmSuppose      <- rule $ AsmSuppose <$> (_suppose *> stmt)
-    asm             <- rule $ assumptionList (asmLet <|> asmSuppose) <* _dot
+    asm             <- rule $ andList1_ (asmLet <|> asmSuppose) <* _dot
     asms            <- rule $ concat <$> many asm
 
     axiom <- rule $ Axiom <$> asms <* optional _then <*> stmt <* _dot
@@ -406,7 +406,7 @@ andList1 item = ((:|) <$> item <*> many (_commaAnd *> item))
 
 -- | Like 'andList1', but drops the information about nonemptiness.
 andList1_ :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [a]
-andList1_ item = toList <$> andList1 item
+andList1_ item = NonEmpty.toList <$> andList1 item
 
 
 commaList :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty a)
@@ -421,9 +421,6 @@ commaList2 :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonE
 commaList2 item = (:|) <$> item <* _comma <*> commaList_ item
 
 
-assumptionList :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [a]
-assumptionList item = NonEmpty.toList <$> andList1 item
-
 enumerated :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [a]
 enumerated p = NonEmpty.toList <$> enumerated1 p
 
-- 
cgit v1.2.3


From 2b2e37e1dc6d74433ef7d455a21f043df8201c3a Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 18 Jun 2024 17:05:44 +0200
Subject: Update topological-space.tex

---
 library/topology/topological-space.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index 2bbdf09..55bc253 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -262,5 +262,5 @@
 \end{proof}
 
 \begin{definition}\label{neighbourhoods}
-    $\neighbourhoods{x}{X} = \{U\in\opens[X] \mid x\in U\}$.
+    $\neighbourhoods{x}{X} = \{N\in\pow{\carrier[X]} \mid \exists U\in\opens[X]. x\in U\subseteq N\}$.
 \end{definition}
-- 
cgit v1.2.3