bc37932 · Idris-dev · git.iko.soy

lib/Prelude/Complex.idr+1−1

compare with master

unifiedsplit

@@ -1,5 +1,5 @@

1{-

3-}

4

5

lib/Prelude/Fin.idr+10−3

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

1module Prelude.Fin

2

3import Prelude.Nat

4+import Prelude.Either

4

5

5data Fin : Nat -> Set where

6data Fin : Nat -> Set where

6 fO : Fin (S k)

7 fO : Fin (S k)

@@ -13,7 +14,13 @@ instance Eq (Fin n) where

13 eq (fS k) (fS k') = eq k k'

14 eq (fS k) (fS k') = eq k k'

14 eq _ _ = False

15 eq _ _ = False

15

16

16−wkn : Fin n -> Fin (S n)

17+weaken : Fin n -> Fin (S n)

17−wkn fO = fO

18+weaken fO = fO

18−wkn (fS k) = fS (wkn k)

19+weaken (fS k) = fS (weaken k)

19

20

21+strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)

22+strengthen {n = S k} fO = Right fO

23+strengthen {n = S k} (fS i) with (strengthen i)

24+ strengthen (fS k) | Left x = Left (fS x)

25+ strengthen (fS k) | Right x = Right (fS x)

26+strengthen f = Left f

src/Idris/ElabDecls.hs+3−1

@@ -626,7 +626,9 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

626 Left _ -> fail $ show fc ++ "with clause does not match top level"

627 Right mvars -> do lhs <- updateLHS n wname mvars ns (fullApp tm) w

628 return $ PWith fc wname lhs ws wval withs'

629−

629+ mkAux wname toplhs ns c

630+ = fail $ show fc ++ "badly formed with clause"

631+

630 updateLHS n wname mvars ns (PApp fc (PRef fc' n') args) w

632 updateLHS n wname mvars ns (PApp fc (PRef fc' n') args) w

631 = let ns' = map (keepMvar (map fst mvars) fc') ns in

633 = let ns' = map (keepMvar (map fst mvars) fc') ns in

632 return $ substMatches mvars $

634 return $ substMatches mvars $