diff options
| author | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-09-18 00:01:42 +0200 |
|---|---|---|
| committer | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-09-18 00:01:42 +0200 |
| commit | c943ca6441e9118bc9caee1c11f697da89bc06b7 (patch) | |
| tree | 1bfff18c501b0b8fa28d54848168d6b9ea06f12c /source/Syntax/Concrete.hs | |
| parent | a9785eb4cac6b8c237173f7e14367babd79e92e1 (diff) | |
working commit
Diffstat (limited to 'source/Syntax/Concrete.hs')
| -rw-r--r-- | source/Syntax/Concrete.hs | 4 |
1 files changed, 2 insertions, 2 deletions
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 |