git.iko.soy/Idris-dev
on master help sign in
Added reg009 for catching unification problem
b1684a7Edwin Brady
test/reg009/expectednew file
compare with master
unifiedsplit

No changes to the content.

test/reg009/reg009.lidrnew file+19
@@ -0,0 +1,19 @@
1+> isAnyBy : (alpha -> Bool) -> (n : Nat ** Vect alpha n) -> Bool
2+> isAnyBy _ (_ ** Nil) = False
3+> isAnyBy p (_ ** (a :: as)) = p a || isAnyBy p (_ ** as)
4+
5+
6+> filterTagP : (p : alpha -> Bool) ->
7+> (as : Vect alpha n) ->
8+> so (isAnyBy p (n ** as)) ->
9+> (m : Nat ** (Vect (a : alpha ** so (p a)) m, so (m > O)))
10+> filterTagP p (a :: as) q with (p a)
11+> | True = (_
12+> **
13+> ((a ** believe_me oh)
14+> ::
15+> (fst (getProof (filterTagP p as (believe_me oh)))),
16+> oh
17+> )
18+> )
19+> | False = filterTagP p as (believe_me oh)
test/reg009/runnew file+3
@@ -0,0 +1,3 @@
1+#!/bin/bash
2+idris $@ reg009.lidr --check
3+rm -f reg009 *.ibc