diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2025-08-12 20:41:44 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2025-08-12 20:41:44 +0200 |
| commit | 0a59ce43beaf13ec25a4483aaf7b8a66d9e4907e (patch) | |
| tree | c35f15e21424bfee311fc51a3e0b5daed464216c /source | |
| parent | 39ef87d3ce39152febc130aa95e25dc0722c3525 (diff) | |
Relax function symbol definitions
Extra assumptions are simply discarded for now.
Diffstat (limited to 'source')
| -rw-r--r-- | source/Syntax/Concrete.hs | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index 3c6700b..8784a1f 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -255,10 +255,11 @@ grammar lexicon@Lexicon{..} = mdo defnHead <- rule $ optional _write *> asum [defnAdj, defnVerb, defnNoun, defnRel, defnSymbolicPredicate] defnIf <- rule $ Defn <$> asms <*> defnHead <* (_iff <|> _if) <*> stmt <* _dot - defnFunSymb <- rule $ _comma *> termExpr <* _comma -- ^ Optional symbolic equivalent. + defnFunSymb <- rule $ _comma *> termExpr <* _comma -- Optional symbolic equivalent. defnFun <- rule $ DefnFun <$> asms <*> (optional _the *> funVar) <*> optional defnFunSymb <* _is <*> term <* _dot symbolicPatternEqTerm <- rule do + asms -- NB assumptions are currently ignored! pat <- beginMath *> symbolicPattern <* _eq e <- expr <* endMath <* _dot pure (pat, e) |