diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2025-07-02 20:28:22 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2025-07-02 20:28:22 +0200 |
| commit | 793849dd0b20bc70ea0e0ecfd5008a3806eca0d9 (patch) | |
| tree | 280949f358a695c5471212cc5b22950399d8cd57 /source/Syntax/Internal.hs | |
| parent | 3caadfbe0fdb417b8edebc17002ddafe795a4bcc (diff) | |
| parent | 8fd49ae84e8cc4524c19b20fa0aabb4e77a46cd5 (diff) | |
Merge pull request #2 from Simon-Kor/main
Merge (finally)
Diffstat (limited to 'source/Syntax/Internal.hs')
| -rw-r--r-- | source/Syntax/Internal.hs | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs index 44603ad..c098380 100644 --- a/source/Syntax/Internal.hs +++ b/source/Syntax/Internal.hs @@ -324,6 +324,16 @@ makeDisjunction = \case [] -> Bottom es -> List.foldl1' Or es +makeIff :: [ExprOf a] -> ExprOf a +makeIff = \case + [] -> Bottom + es -> List.foldl1' Iff es + +makeXor :: [ExprOf a] -> ExprOf a +makeXor = \case + [] -> Bottom + es -> List.foldl1' Xor es + finiteSet :: NonEmpty (ExprOf a) -> ExprOf a finiteSet = foldr cons EmptySet where @@ -436,6 +446,8 @@ data Proof | Define VarSymbol Term Proof | DefineFunction VarSymbol VarSymbol Term Term Proof + | DefineFunctionLocal VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof + deriving instance Show Proof deriving instance Eq Proof deriving instance Ord Proof |