git.iko.soy/Idris-dev
on master help sign in
Add Fin.strengthen
commitbc3793244402913279213a7f48026eee4ca44572 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 23 Nov 2012, 15:47 (14 years ago) parentaf71c77
3 files changed+14−5
compare with master
unifiedsplit
lib/Prelude/Complex.idr+1−1 lib/Prelude/Fin.idr+10−3 src/Idris/ElabDecls.hs+3−1
lib/Prelude/Complex.idr+1−1
@@ -1,5 +1,5 @@
11{-
2− © 2012 Copyright Mekeor Melire
2+ (c) 2012 Copyright Mekeor Melire
33-}
44
55
lib/Prelude/Fin.idr+10−3
@@ -1,6 +1,7 @@
11module Prelude.Fin
22
33import Prelude.Nat
4+import Prelude.Either
45
56data Fin : Nat -> Set where
67 fO : Fin (S k)
@@ -13,7 +14,13 @@ instance Eq (Fin n) where
1314 eq (fS k) (fS k') = eq k k'
1415 eq _ _ = False
1516
16−wkn : Fin n -> Fin (S n)
17−wkn fO = fO
18−wkn (fS k) = fS (wkn k)
17+weaken : Fin n -> Fin (S n)
18+weaken fO = fO
19+weaken (fS k) = fS (weaken k)
1920
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)
626626 Left _ -> fail $ show fc ++ "with clause does not match top level"
627627 Right mvars -> do lhs <- updateLHS n wname mvars ns (fullApp tm) w
628628 return $ PWith fc wname lhs ws wval withs'
629−
629+ mkAux wname toplhs ns c
630+ = fail $ show fc ++ "badly formed with clause"
631+
630632 updateLHS n wname mvars ns (PApp fc (PRef fc' n') args) w
631633 = let ns' = map (keepMvar (map fst mvars) fc') ns in
632634 return $ substMatches mvars $