2ce525e · Idris-dev · git.iko.soy

lib/prelude/list.idr+2−2

compare with master

unifiedsplit

@@ -12,11 +12,11 @@ data List a = Nil | (::) a (List a)

12rev : List a -> List a

13rev xs = revAcc [] xs where

14 revAcc : List a -> List a -> List a

15− revAcc acc [] = acc

15+ revAcc acc [] = acc

16 revAcc acc (x :: xs) = revAcc (x :: acc) xs

17

18app : List a -> List a -> List a

19−app [] xs = xs

19+app [] xs = xs

20app (x :: xs) ys = x :: app xs ys

21

22length : List a -> Int

lib/prelude/nat.idr+2−6

@@ -100,9 +100,7 @@ mult_commutes O m = ?mult_commO

100mult_commutes (S k) m = let ih = mult_commutes k m in ?mult_commSk

101

102mult_commSk = proof {

103− intro;

103+ intros;

104− intro;

105− intro;

106 rewrite sym ih;

104 rewrite sym ih;

107 rewrite multn_Sm m k;

105 rewrite multn_Sm m k;

108 trivial;

106 trivial;

@@ -115,9 +113,7 @@ mult_commO = proof {

115}

113}

116

114

117multnSmSk = proof {

115multnSmSk = proof {

118− intro;

116+ intros;

119− intro;

120− intro;

121 rewrite plus_commutes (mult k m) m;

117 rewrite plus_commutes (mult k m) m;

122 rewrite sym (plus_assoc k (mult k m) m);

118 rewrite sym (plus_assoc k (mult k m) m);

123 rewrite ih;

119 rewrite ih;

lib/prelude/vect.idr+19

@@ -31,4 +31,23 @@ map : (a -> b) -> Vect a n -> Vect b n

31map f [] = []

32map f (x :: xs) = f x :: map f xs

33

34+rev : Vect a n -> Vect a n

35+rev xs = revAcc [] xs where

36+ revAcc : Vect a n -> Vect a m -> Vect a (n + m)

37+ revAcc acc [] ?= acc

38+ revAcc acc (x :: xs) ?= revAcc (x :: acc) xs

39+

40+---------- Proofs ----------

41+

42+revAcc_lemma_2 = proof {

43+ intros;

44+ rewrite sym (plusn_Sm n k);

45+ exact value;

46+}

47+

48+revAcc_lemma_1 = proof {

49+ intros;

50+ rewrite sym (plusnO n);

51+ exact value;

52+}

34

53

src/Core/TT.hs+8−1

@@ -267,11 +267,18 @@ instance Show UConstraint where

267type UCs = (Int, [UConstraint])

268

269data NameType = Bound | Ref | DCon Int Int | TCon Int Int

270− deriving (Show, Eq)

270+ deriving (Show)

271{-!

272deriving instance Binary NameType

273!-}

274

275+instance Eq NameType where

276+ Bound == Bound = True

277+ Ref == Ref = True

278+ DCon _ a == DCon _ b = (a == b) -- ignore tag

279+ TCon _ a == TCon _ b = (a == b) -- ignore tag

280+ _ == _ = False

281+

275data TT n = P NameType n (TT n) -- embed type

282data TT n = P NameType n (TT n) -- embed type

276 | V Int

283 | V Int

277 | Bind n (Binder (TT n)) (TT n)

284 | Bind n (Binder (TT n)) (TT n)

src/Idris/AbsSyntax.hs+1−1

@@ -460,7 +460,7 @@ mapPT f t = f (mpt t) where

460 mpt x = x

461

462

463−data PTactic' t = Intro [Name] | Focus Name

463+data PTactic' t = Intro [Name] | Intros | Focus Name

464 | Refine Name [Bool] | Rewrite t | LetTac Name t

465 | Exact t | Compute | Trivial

466 | Solve

src/Idris/ElabTerm.hs+7

@@ -371,6 +371,13 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

371 bname (Bind n _ _) = Just n

372 bname _ = Nothing

373 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

374+ runT Intros = do g <- goal

375+ attack; intro (bname g)

376+ try (runT Intros)

377+ (return ())

378+ where

379+ bname (Bind n _ _) = Just n

380+ bname _ = Nothing

374 runT (Exact tm) = do elab ist toplevel False False (MN 0 "tac") tm

381 runT (Exact tm) = do elab ist toplevel False False (MN 0 "tac") tm

375 when autoSolve solveAll

382 when autoSolve solveAll

376 runT (Refine fn [])

383 runT (Refine fn [])

src/Idris/Parser.hs+1

@@ -1124,6 +1124,7 @@ pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

1124pTactic :: SyntaxInfo -> IParser PTactic

1125pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

1126 return $ Intro ns

1127+ <|> do reserved "intros"; return Intros

1127 <|> try (do reserved "refine"; n <- pName

1128 <|> try (do reserved "refine"; n <- pName

1128 imps <- many1 imp

1129 imps <- many1 imp

1129 return $ Refine n imps)

1130 return $ Refine n imps)

tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/miscellany.tex+1−2

@@ -176,8 +176,7 @@ Universes are \emph{cumulative}, that is, if \texttt{x : Set n} we can also have

176The typechecker generates such universe

177constraints and reports an error if any inconsistencies are found. Ordinarily, a

178programmer does not need to worry about this, but it does prevent (contrived)

179−programs such as

179+programs such as the following:

180−the following:

181

180

182\begin{SaveVerbatim}{idid}

181\begin{SaveVerbatim}{idid}

183

182

tutorial/theorems.tex+2−3

@@ -241,7 +241,7 @@ Let us now prove the other required lemma, \texttt{plusredO\_S}:

241In this case, the goal is a function type, using \texttt{k} (the argument accessible by

242pattern matching) and \texttt{ih} (the local variable containing the result of

243the recursive call). We can introduce these as premisses using the \texttt{intro} tactic

244−twice. This gives:

244+twice (or \texttt{intros}, which introduces all arguments as premisses). This gives:

245

246\begin{SaveVerbatim}{prSintros}

247

@@ -282,8 +282,7 @@ the goal using that proof. Here, it results in an equality which is trivially pr

282plusredO_S: no more goals

283-plusredO_S> qed

284plusredO_S = proof {

285− intro;

285+ intros;

286− intro;

287 rewrite ih;

286 rewrite ih;

288 trivial;

287 trivial;

289}

288}