@@ -179,13 +179,13 @@ internalExpr syn =
179 <|> try (unifyLog syn)
179 <|> try (unifyLog syn)
180 <|> try (noImplicits syn)
180 <|> try (noImplicits syn)
181 <|> recordType syn
181 <|> recordType syn
182− <|> try (simpleExpr syn)
183 <|> lambda syn
182 <|> lambda syn
184 <|> quoteGoal syn
183 <|> quoteGoal syn
185 <|> let_ syn
184 <|> let_ syn
186 <|> rewriteTerm syn
185 <|> rewriteTerm syn
187− <|> pi syn
186+ <|> try(pi syn)
188 <|> doBlock syn
187 <|> doBlock syn
189 <?> "expression"
189 <?> "expression"
191{- | Parses a case expression
191{- | Parses a case expression
@@ -266,22 +266,22 @@ simpleExpr syn =
266 <|> proofExpr syn
266 <|> proofExpr syn
267 <|> tacticsExpr syn
267 <|> tacticsExpr syn
268 <|> caseExpr syn
268 <|> caseExpr syn
269+ <|> do reserved "Type"; return PType
269− <|> try (do fc <- getFC
270+ <|> do fc <- getFC
270− x <- fnName
271+ x <- fnName
271− return (PRef fc x))
272+ return (PRef fc x)
272 <|> try (listExpr syn)
273 <|> try (listExpr syn)
273 <|> try (comprehension syn)
274 <|> try (comprehension syn)
274− <|> try (alt syn)
275+ <|> alt syn
275− <|> try (idiom syn)
276+ <|> idiom syn
276 <|> do lchar '('
277 <|> do lchar '('
277 bracketed (disallowImp syn)
278 bracketed (disallowImp syn)
278− <|> try (do c <- constant
279+ <|> do c <- constant
279− fc <- getFC
280+ fc <- getFC
280− return (modifyConst syn fc (PConstant c)))
281+ return (modifyConst syn fc (PConstant c))
281− <|> do reserved "Type"; return PType
282− <|> try (do symbol "_|_"
282+ <|> do symbol "_|_"
283− fc <- getFC
283+ fc <- getFC
284− return (PFalse fc))
284+ return (PFalse fc)
285 <|> do lchar '_'; return Placeholder
285 <|> do lchar '_'; return Placeholder
286 <|> simpleExternalExpr syn
286 <|> simpleExternalExpr syn
287 <?> "expression"
287 <?> "expression"