diff options
Diffstat (limited to 'source/Syntax/Abstract.hs')
| -rw-r--r-- | source/Syntax/Abstract.hs | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index c8d5dac..23da652 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -338,6 +338,10 @@ data Defn | DefnOp SymbolPattern Expr deriving (Show, Eq, Ord) +data CalcQuantifier + = CalcQuantifier (NonEmpty VarSymbol) Bound (Maybe Stmt) + deriving (Show, Eq, Ord) + data Proof = Omitted | Qed Justification @@ -351,7 +355,7 @@ data Proof | Assume Stmt Proof | FixSymbolic (NonEmpty VarSymbol) Bound Proof | FixSuchThat (NonEmpty VarSymbol) Stmt Proof - | Calc Calc Proof + | Calc (Maybe CalcQuantifier) Calc Proof -- ^ Simplify goals that are implications or disjunctions. | TakeVar (NonEmpty VarSymbol) Bound Stmt Justification Proof | TakeNoun (NounPhrase []) Justification Proof |