diff options
Diffstat (limited to 'source')
| -rw-r--r-- | source/Checking.hs | 2 | ||||
| -rw-r--r-- | source/Meaning.hs | 4 | ||||
| -rw-r--r-- | source/Syntax/Abstract.hs | 2 | ||||
| -rw-r--r-- | source/Syntax/Concrete.hs | 4 | ||||
| -rw-r--r-- | source/Syntax/Internal.hs | 2 |
5 files changed, 7 insertions, 7 deletions
diff --git a/source/Checking.hs b/source/Checking.hs index 766c327..8bc38a4 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -543,7 +543,7 @@ checkProof = \case checkCalc calc assume [Asm (calcResult calc)] checkProof continue - DefineFunctionMathy funVar argVar domVar ranExpr definitions continue -> do + DefineFunctionLocal funVar argVar domVar ranExpr definitions continue -> do -- We have f: X \to Y and x \mapsto ... -- definition is a nonempty list of (expresssion e, formula phi) -- such that f(x) = e if phi(x) diff --git a/source/Meaning.hs b/source/Meaning.hs index 4a21fa3..00a944f 100644 --- a/source/Meaning.hs +++ b/source/Meaning.hs @@ -606,9 +606,9 @@ glossProof = \case then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof else error "mismatched variables in function definition." - Raw.DefineFunctionMathy funVar domVar ranExpr funVar2 argVar definitions proof -> do + Raw.DefineFunctionLocal funVar domVar ranExpr funVar2 argVar definitions proof -> do if funVar == funVar2 - then Sem.DefineFunctionMathy funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof + then Sem.DefineFunctionLocal funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof else error "missmatched function names" Raw.Calc calc proof -> Sem.Calc <$> glossCalc calc <*> glossProof proof diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index 13691e7..c8022c7 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -373,7 +373,7 @@ data Proof - | DefineFunctionMathy VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof + | DefineFunctionLocal VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains. -- deriving (Show, Eq, Ord) diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index 7a89bea..9b947b0 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -374,7 +374,7 @@ grammar lexicon@Lexicon{..} = mdo -- \end{cases} functionDefineCase <- rule $ (,) <$> (optional _ampersand *> expr) <*> (_ampersand *> text _if *> formula) - defineFunctionMathy <- rule $ DefineFunctionMathy + defineFunctionLocal <- rule $ DefineFunctionLocal <$> (_define *> beginMath *> varSymbol) -- Define $ f <*> (_colon *> varSymbol) -- : 'var' \to 'var' <*> (_to *> expr <* endMath <* _suchThat) @@ -386,7 +386,7 @@ grammar lexicon@Lexicon{..} = mdo - proof <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionMathy, qed] + proof <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionLocal, qed] blockAxiom <- rule $ uncurry3 BlockAxiom <$> envPos "axiom" axiom diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs index e83126d..c098380 100644 --- a/source/Syntax/Internal.hs +++ b/source/Syntax/Internal.hs @@ -446,7 +446,7 @@ data Proof | Define VarSymbol Term Proof | DefineFunction VarSymbol VarSymbol Term Term Proof - | DefineFunctionMathy VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof + | DefineFunctionLocal VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof deriving instance Show Proof deriving instance Eq Proof |