Skip to content

Commit

Permalink
[ experim ] A silly experiment
Browse files Browse the repository at this point in the history
  • Loading branch information
buzden committed Sep 12, 2023
1 parent 9919039 commit 72fed15
Showing 1 changed file with 4 additions and 2 deletions.
6 changes: 4 additions & 2 deletions src/Idris/Parser.idr
Original file line number Diff line number Diff line change
Expand Up @@ -399,8 +399,10 @@ mutual
<|> do b <- bounds (continueWith indents ")")
pure (PUnit (boundToFC fname (mergeBounds s b)))
-- dependent pairs with type annotation (so, the type form)
<|> do dpairType fname s indents <* (decorate fname Typ $ symbol ")")
<* actD (toNonEmptyFC $ boundToFC fname s, Typ, Nothing)
<|> do t <- dpairType fname s indents
decorate fname Typ $ symbol ")"
actD (toNonEmptyFC $ boundToFC fname s, Typ, Nothing)
pure t
<|> do e <- bounds (typeExpr pdef fname indents)
-- dependent pairs with no type annotation
(do loc <- bounds (symbol "**")
Expand Down

0 comments on commit 72fed15

Please sign in to comment.