c37de47 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+8−1

@@ -1061,7 +1061,14 @@ expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)

1061 (map econ cons)

1062 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)

1063 econ (doc, n, t, fc, fs)

1064− = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)

1064+ = (doc, dec n, piBindp impl ps (expandParams dec ps ns [] t), fc, fs)

1065+expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)

1066+ = if tn `elem` ns

1067+ then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))

1068+ cdoc (dec cn) conty

1069+ else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)

1070+ cdoc (dec cn) conty

1071+ where conty = piBindp impl ps (expandParams dec ps ns [] cty)

1065expandParamsD rhs ist dec ps ns (PParams f params pds)

1072expandParamsD rhs ist dec ps ns (PParams f params pds)

1066 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

1073 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

1067 (map (expandParamsD True ist dec ps ns) pds)

1074 (map (expandParamsD True ist dec ps ns) pds)

src/Idris/Completion.hs+1−1

@@ -50,7 +50,7 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)

50 , (":e", Just ExprTArg)

51 , (":eval", Just ExprTArg)

52 ] ++ map (\x -> (x, Nothing)) [

53− "intros", "compute", "trivial", "solve", "attack",

53+ "intros", "compute", "trivial", "search", "solve", "attack",

54 "state", "term", "undo", "qed", "abandon", ":q"

55 ]

56tactics = map fst tacticArgs

src/Idris/ParseExpr.hs+2

@@ -1165,6 +1165,8 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

1165 return $ TSeq t (mergeSeq ts)

1166 <|> do reserved "compute"; return Compute

1167 <|> do reserved "trivial"; return Trivial

1168+ <|> do reserved "search"; n <- (indentPropHolds gtProp *> fnName)

1169+ return (ProofSearch Nothing n [])

1168 <|> do reserved "instance"; return TCInstance

1170 <|> do reserved "instance"; return TCInstance

1169 <|> do reserved "solve"; return Solve

1171 <|> do reserved "solve"; return Solve

1170 <|> do reserved "attack"; return Attack

1172 <|> do reserved "attack"; return Attack