1d76cd3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix checked vs inferred bug

commit1d76cd3cb310916829543c7cc7e70f7f176e445d authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 17 Jan 2012, 16:43 (15 years ago) parent566616c

3 files changed+7−3

unifiedsplit

src/Idris/AbsSyntax.hs+5−1

@@ -1215,7 +1215,11 @@ matchClause' names x y = checkRpts $ match (fullApp x) (fullApp y) where

12151215 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

12161216 fullApp x = x

12171217

1218− match' x y = match (fullApp x) (fullApp y)

1218+ match' x y = match (fullApp x) (fullApp y)

1219+ match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'

1220+ | PConstant (I _) <- getTm x = match (getTm x) x'

1221+ match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])

1222+ | PConstant (I _) <- getTm x = match (getTm x) x'

12191223 match (PApp _ f args) (PApp _ f' args')

12201224 | length args == length args'

12211225 = do mf <- match' f f'

tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/typesfuns.tex+2−2

@@ -419,7 +419,7 @@ definition, which defines a predicate on vectors:

419419

420420\begin{SaveVerbatim}{elem}

421421

422−data Elem : a -> (Vect a n) -> Set where

422+data Elem : a -> Vect a n -> Set where

423423 here : {x:a} -> {xs:Vect a n} -> Elem x (x :: xs)

424424 there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs)

425425

@@ -451,7 +451,7 @@ ordering of any implicit arguments which can appear within the block:

451451\begin{SaveVerbatim}{elemusing}

452452

453453using (x:a, y:a, xs:Vect a n)

454− data Elem : a -> (Vect a n) -> Set where

454+ data Elem : a -> Vect a n -> Set where

455455 here : Elem x (x :: xs)

456456 there : Elem x xs -> Elem x (y :: xs)

457457