430eab9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow postulates in where/parameters blocks

430eab9Edwin Brady14 years ago

src/Idris/AbsSyntax.hs+7

@@ -511,6 +511,13 @@ expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)

511 PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))

512 else --trace (show (n, expandParams dec ps ns ty)) $

513 PTy doc syn fc o n (expandParams dec ps ns ty)

514+expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)

515+ = if n `elem` ns && (not rhsonly)

516+ then -- trace (show (n, expandParams dec ps ns ty)) $

517+ PPostulate doc syn fc o (dec n) (piBind ps

518+ (expandParams dec ps ns ty))

519+ else --trace (show (n, expandParams dec ps ns ty)) $

520+ PPostulate doc syn fc o n (expandParams dec ps ns ty)

514expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

521expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

515 = let n' = if n `elem` ns then dec n else n in

522 = let n' = if n `elem` ns then dec n else n in

516 PClauses fc opts n' (map expandParamsC cs)

523 PClauses fc opts n' (map expandParamsC cs)