Desugar in default argument values
commite9ff42dc1b148a135df0d03bbcba5cac8fbae12c
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateMon 2 Mar 2015, 16:57 (12 years ago)
parent0222187
src/Idris/ParseExpr.hs+3−1
@@ -878,7 +878,9 @@ pi syn =
878878 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do
879879 try (lchar '{' *> reserved "default")
880880 when (st == Static) $ fail "default tactic constraints can not be static"
881− script <- simpleExpr syn
881+ ist <- get
882+ script' <- simpleExpr syn
883+ let script = debindApp syn . desugar syn ist $ script'
882884 xt <- typeDeclList syn
883885 lchar '}'
884886 symbol "->"