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

src/Idris/AbsSyntax.hs+5−1

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

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

1216 fullApp x = x

1217

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'

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

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

1220 | length args == length args'

1224 | length args == length args'

1221 = do mf <- match' f f'

1225 = 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:

419

420\begin{SaveVerbatim}{elem}

421

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

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

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

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

425

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

451\begin{SaveVerbatim}{elemusing}

452

453using (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

455 here : Elem x (x :: xs)

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

457