3629548 · Idris-dev · git.iko.soy

src/Idris/Elab/Rewrite.hs+3−3

@@ -76,9 +76,9 @@ elabRewrite elab ist fc substfn_in rule sc_in newg

76 when (g == pred_tt) $ lift $ tfail (NoRewriting l r g)

77 let pred = PLam fc rname fc Placeholder

78 (delab ist pred_tt)

79− let rewrite = stripImpls $

80− addImplBound ist (map fstEnv env) (PApp fc (PRef fc [] substfn)

79+ let rewrite = addImplBound ist (map fstEnv env) (PApp fc (PRef fc [] substfn)

80+ [pexp (stripImpls pred),

81− [pexp pred, pexp rule, pexp sc])

81+ pexp (stripImpls rule), pexp sc])

82-- trace ("LHS: " ++ show l ++ "\n" ++

83-- "RHS: " ++ show r ++ "\n" ++

84-- "REWRITE: " ++ show rewrite ++ "\n" ++

test/regression001/reg006.idrnew file+14

@@ -0,0 +1,14 @@

1+module Parity

2+

3+data Parity : Nat -> Type where

4+ Even : Parity (n + n)

5+ Odd : Parity (S (plus n n))

6+

7+parity : (n:Nat) -> Parity n

8+parity Z = Even {n = Z}

9+parity (S Z) = Odd {n = Z}

10+parity (S (S k)) with (parity k)

11+ parity (S (S (j + j))) | Even

12+ = rewrite plusSuccRightSucc j j in (Even {n = S j})

13+ parity (S (S (S (plus j j)))) | Odd

14+ = rewrite plusSuccRightSucc j j in (Odd {n = S j})

test/regression001/run+1−1

@@ -1,7 +1,7 @@

1#!/usr/bin/env bash

2${IDRIS:-idris} $@ --check \

3 reg001.idr reg002.idr reg003.idr reg004.lidr reg005.idr \

4− reg036.idr reg037.idr reg038.idr reg046.idr \

4+ reg006.idr reg036.idr reg037.idr reg038.idr reg046.idr \

5 reg047a.idr reg053.idr reg057.idr reg058.idr reg058a.idr \

6 reg059.idr reg060.idr reg061.idr reg062.idr reg063.idr \

7 reg064.idr reg065.idr reg066.idr reg071.idr reg074.idr \