idris.log

running tests
Running 1 test suites...
Test suite regression-and-sanity-tests: RUNNING...
basic001 finished...FAILURE
0a1,2
> 1f4o1b4a1r1b3a1z
> 1f4o1b4a1r1b3a1z
basic002 finished...FAILURE
0a1,5
> test006.idr:25:23-28:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> test006.idr:32:23-28:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> [False, True, False, True, False, True]
basic003 finished...FAILURE
0a1,3
> [1, 1, 3, 5, 5, 8, 9]
> 55
> 3628800
basic004 finished...FAILURE
0a1
> [10, 11, 12, 13, 14, 15, 16, 17, 18, 19]
basic005 finished...FAILURE
0a1
> 1
basic006 finished...FAILURE
0a1,11
> test020a.idr:16:18:
> When checking right hand side of foo with expected type
>         List a
> 
> When checking an application of function Prelude.List.reverse:
>         Type mismatch between
>                 Vect n a (Type of xs)
>         and
>                 List a (Expected type)
> [3, 2, 1]
> "Number 42"
basic007 finished...FAILURE
0a1
> True
basic008 finished...FAILURE
0a1
> Just 2
basic009 finished...FAILURE
0a1,16
> MAIN-PASS
> Faulty.idr:7:7:
> When checking right hand side of fault with expected type
>         num = 0
> 
> Type mismatch between
>         0 = 0 (Type of Refl)
> and
>         num = 0 (Expected type)
> 
> Specifically:
>         Type mismatch between
>                 0
>         and
>                 num
> Multiple.idr:3:1:import alias not unique: "X"
basic010 finished...FAILURE
0a1,3
> *oink*
> 10000
> Axiom 10000
basic011 finished...FAILURE
0a1,10
> 6EA049D797FA18D6
> 6EA049D797FA18D6
> FDA01C93B78A192F
> AD85270E93646134
> 6EA049D797FA18D6
> 6EA049D797FA18D6
> 6EA049D797FA18D6
> 6EA049D797FA18D6
> 6EA049D797FA18D6
> 6EA049D797FA18D6
basic012 finished...FAILURE
0a1,2
> 4242
> [1, 2, 3, 4, 5, 6]
basic013 finished...FAILURE
0a1,14
> λx→x
> λx→xλx→x
> x→xλx→xλ
> 4
> '\955'
> λx→xλx→xλx→xλx→xλx→x
> '\955'
> 20
> '\955'
> λ
> Tail: x→xλx→xλx→xλx→xλx→x
> Tail Tail: →xλx→xλx→xλx→xλx→x
> Cons: λλx→xλx→xλx→xλx→xλx→x
> Reverse: x→xλx→xλx→xλx→xλx→xλ
basic014 finished...success
basic015 finished...FAILURE
0a1,3
> Rows: Columns: [[0, 1, 2, 3, 4, 5], [6, 7, 8, 9, 10, 11], [12, 13, 14, 15, 16, 17], [18, 19, 20, 21, 22, 23], [24, 25, 26, 27, 28, 29]]
> Transposed:
> [[0, 6, 12, 18, 24], [1, 7, 13, 19, 25], [2, 8, 14, 20, 26], [3, 9, 15, 21, 27], [4, 10, 16, 22, 28], [5, 11, 17, 23, 29]]
basic016 finished...FAILURE
0a1
> Cycle detected in imports: CycleA.idr -> CycleB -> CycleC -> CycleA -> CycleB
basic017 finished...FAILURE
0a1,3
> basic017a.idr:11:8:When checking type of Main.append:
> When checking an application of Main.Vect:
>         No such variable n
bignum001 finished...FAILURE
0a1
> OK
bignum002 finished...FAILURE
0a1
> 19827346982734
bounded001 finished...FAILURE
0a1,6
> FFFF
> 0000
> FFFFFFFF
> 00000000
> FFFFFFFFFFFFFFFF
> 0000000000000000
classes001 finished...FAILURE
0a1,29
> Interface MyShow
>     A fancy shower with a constructor
> 
> Parameters:
>     a   -- the thing to be shown
> 
> Methods:
>     myShow : MyShow a => (x : a) -> String
>         The shower
>         
>         The function is Total
> Implementation constructor:
>     MkMyShow : (myShow : a -> String) -> MyShow a
>         Build a MyShow
>         Arguments:
>             (implicit) a : Type  -- the thing to be shown
>             
>             myShow : a -> String  -- The shower
>             
> Implementations:
>     MyShow Integer
> MkMyShow : (myShow : a -> String) -> MyShow a
>     Build a MyShow
>     Arguments:
>         (implicit) a : Type  -- the thing to be shown
>         
>         myShow : a -> String  -- The shower
>         
>     The function is Total
corecords001 finished...FAILURE
0a1,5
> 0
> 1
> 3
> 1
> 0
corecords002 finished...FAILURE
0a1,3
> "Foo"
> "Foo"
> "Foo"
delab001 finished...FAILURE
0a1,12
> foo : Nat -> String
> foo n = case n of
>           0 => "z"
>           S _ => "s"
> bar : Nat -> String -> String
> bar x y = case x of
>             0 => y
>             S _ => (y ++ y)
> append : List a -> List a -> List a
> append xs ys = case xs of
>                  [] => ys
>                  (x :: xs) => (x :: (append xs ys))
disambig002 finished...success
docs001 finished...FAILURE
0a1,17
> Interface C
>     interface
> 
> Parameters:
>     t   -- a type
> 
> Methods:
>     m : C t => t
>         member of interface
>         
>         The function is Total
> Implementations:
>     C A
>         implementation of interface
>     C (D a b)
>         another implementation of interface
>         a   -- parameter type
docs002 finished...FAILURE
0a1,12
> T1 : Type
>     Some documentation
>     
>     The function is Total
> T2 : Type
>     Some other documentation
>     
>     The function is Total
> T3 : Int
>     Some provided postulate
>     
>     The function is not yet checked for totality
docs003 finished...FAILURE
0a1,39
> Interface Functor
>     Functors allow a uniform action over a parameterised type.
> 
> Parameters:
>     f   -- a parameterised type
> 
> Methods:
>     map : Functor f => (func : a -> b) -> f a -> f b
>         Apply a function across everything of type 'a' in a
>         parameterised type
>         
>         The function is Total
> Implementations:
>     Functor List
>     Functor (IO' ffi)
>     Functor Stream
>     Functor Provider
>     Functor Binder
>     Functor Elab
>     Functor PrimIO
>     Functor Maybe
>     Functor (Either e)
> 
> Named implementations:
>     docs003.mine : Functor List
>     docs003.another : Functor List
>         More functors!
> 
> Child interfaces:
>     Traversable f
>     Applicative f
> Named instance:
>     docs003.mine : Functor List
>         
>         
> Named instance:
>     docs003.another : Functor List
>         More functors!
>         
docs004 finished...FAILURE
0a1,18
> Main.MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a
>     Constructor for Foo
>     Arguments:
>         (implicit) a : Type  -- a type
>         
>         bar : Nat  -- A field bar
>         
>         baz : Bool  -- A field baz
>         
>     The function is Total
> Main.Foo.bar : (rec : Foo a) -> Nat
>     A field bar
>     
>     The function is Total
> Main.Foo.baz : (rec : Foo a) -> Bool
>     A field baz
>     
>     The function is Total
dsl001 finished...FAILURE
0a1,2
> 24
> 12
dsl002 finished...FAILURE
0a1
> foo
dsl003 finished...FAILURE
0a1,2
> ForAll INT (ForAll INT (ItHolds (Var (FS FZ) === Var FZ))) : Spec []
> Refl : ARR BOOL (ARR INT UNIT) = ARR BOOL (ARR INT UNIT)
dsl004 finished...success
effects001 finished...FAILURE
0a1,4
> ["HELLO!!!\n", "WORLD!!!\n", ""]
> 3
> 15
> Answer: 99
effects002 finished...FAILURE
0a1
> [1, 2, 3, 4]
effects003 finished...FAILURE
0a1,43
> hangman.idr:204:8-13:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> ------------
> 
> 6 guesses left
> Enter guess: No, sorry
> ------------
> 
> 5 guesses left
> Enter guess: Good guess!
> ----ee------
> 
> 5 guesses left
> Enter guess: Good guess!
> ----ee---i--
> 
> 5 guesses left
> Enter guess: Good guess!
> -o--ee---i--
> 
> 5 guesses left
> Enter guess: Good guess!
> -offee---i--
> 
> 5 guesses left
> Enter guess: Good guess!
> coffee-c-i--
> 
> 5 guesses left
> Enter guess: Good guess!
> coffeesc-i--
> 
> 5 guesses left
> Enter guess: Good guess!
> coffeesc-ip-
> 
> 5 guesses left
> Enter guess: Good guess!
> coffeescrip-
> 
> 5 guesses left
> Enter guess: Good guess!
> You won! Successfully guessed coffeescript
effects004 finished...FAILURE
0a1,11
> Off we go!
> Counter at 0
> Counter at 1
> Counter at 2
> Counter at 3
> Counter at 4
> Counter at 5
> Counter at 6
> Counter at 7
> Counter at 8
> Finished!
effects005 finished...FAILURE
0a1,5
> WARN : Doing the double with 3
> 6
> 8
> WARN : ["NumOPS"] : Doing the double with 3
> 6
error001 finished...FAILURE
0a1,8
> test002.idr:1:6:Universe inconsistency.
>         Working on: z
>         Old domain: (6,6)
>         New domain: (6,5)
>         Involved constraints: 
>                 ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}
>                 ConstraintFC {uconstraint = y < z, ufc = test002.idr:1:6}
>                 ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}
error002 finished...success
error003 finished...FAILURE
0a1,5
> ErrorReflection.idr:68:5:
> When checking right hand side of bad with expected type
>         Tm [] TUnit
> 
> DSL type error: (t(504) => t'(503)) doesn't match ()
error004 finished...FAILURE
0a1,12
> FunErrTest.idr:35:17:
> When checking right hand side of badCadr1 with expected type
>         Int
> 
> When checking argument cons2 to function FunErrTest.cadr:
>         Could not prove that [] has at least two elements.
> FunErrTest.idr:38:17:
> When checking right hand side of badCadr2 with expected type
>         Int
> 
> When checking argument cons2 to function FunErrTest.cadr:
>         Could not prove that [] has at least two elements.
error005 finished...FAILURE
0a1,36
> error005.idr:13:1:
> When checking right hand side of two with expected type
>         Fin 2
> 
> When checking argument prf to function Data.Fin.fromInteger:
>         When using 2 as a literal for a Fin 2 
>                 2 is not strictly less than 2
> error005.idr:16:1:
> When checking right hand side of hahaha with expected type
>         Fin n
> 
> When checking argument prf to function Data.Fin.fromInteger:
>         When using 0 as a literal for a Fin n 
>                 0 is not strictly less than n
> error005.idr:22:1:
> When checking right hand side of notOk with expected type
>         Fin (plus 2 n)
> 
> When checking argument prf to function Data.Fin.fromInteger:
>         When using 2 as a literal for a Fin (S (S n)) 
>                 2 is not strictly less than S (S n)
> error005.idr:23:24:
> When checking right hand side of b0rken with expected type
>         Fin 3
> 
> When checking argument prf to function Data.Fin.fromInteger:
>         When using n as a literal for a Fin 3 
>                 Could not show that n is less than 3 because n is a bound
>                 variable instead of a constant Integer
> error005.idr:28:1:
> When checking right hand side of x with expected type
>         Fin 4
> 
> When checking argument prf to function Data.Fin.fromInteger:
>         When using 5 as a literal for a Fin 4 
>                 5 is not strictly less than 4
error006 finished...FAILURE
0a1,2
> WithPatsNoWith.idr:4:5:When checking left hand side of foo:
> unexpected patterns outside of "with" block
ffi001 finished...FAILURE
0a1
> 0.9995736030415051
ffi002 finished...FAILURE
0a1
> test023.idr:20:21:Type provider error: Always fails
ffi003 finished...FAILURE
0a1
> testtest
ffi004 finished...success
ffi005 finished...FAILURE
0a1
> oops
ffi006 finished...FAILURE
0a1,2
> Ready to show...
> [10, 20, 30, 40]
folding001 finished...FAILURE
0a1,4
> ([], []) -> ([], [])
> ([1], [1]) -> ([1], [1])
> ([1, 2, 3], [1, 2, 3]) -> ([1, 2, 3], [1, 2, 3])
> ([3, 2, 1], [3, 2, 1]) -> ([3, 2, 1], [3, 2, 1])
idrisdoc001 finished...FAILURE
0a1,3
> Warning: Ignoring empty or non-existing namespace 'TestEmpty'
> Warning: Ignoring empty or non-existing namespace 'TestPrivate'
> No namespaces to generate documentation for
idrisdoc002 finished...FAILURE
0a1
> Functions are documented
idrisdoc003 finished...FAILURE
0a1
> Data types are documented
idrisdoc004 finished...FAILURE
0a1
> Typeclasses are documented
idrisdoc005 finished...FAILURE
0a1,2
> TestTracing: Check
> Prelude.Bool: Check
idrisdoc006 finished...FAILURE
1,2c1,5
< A.fully.Qualified.NAME is NOT in the index
< B is NOT in the index
---
> IdrisDoc file written
> A.fully.Qualified.NAME.html
> B.html
> A.fully.Qualified.NAME is in the index
> B is in the index
idrisdoc007 finished...FAILURE
1c1
< Exit status (expects 1): 127
---
> Exit status (expects 1): 1
idrisdoc008 finished...FAILURE
0a1,2
> Abstract members are documented
> Public members are documented
idrisdoc009 finished...FAILURE
0a1,28
> Data type Test.Test : Type
>     Docs for datatype Test.
>     
> Constructors:
>     MkTest : Test
>         
>         
> Module Test:
>     Docs for module Test.
>     
>     It is a great module. Prelude thingy:
>     
>         > "foo" ++ "bar"
>         "foobar"
>     
>     Imported thingy:
>     
>         > 0.0 :+ 0.2
>         0.0 :+ 0.2
>     
>     Type error:
>     
>         "foo" + 2
>     
>     From this module:
>     
>         > MkTest
>         MkTest
interactive001 finished...FAILURE
0a1,19
> isElem x [] = ?isElem_rhs_1
> isElem x (y :: xs) = ?isElem_rhs_3
> 
>    localZipWith f (_ :: _) (x :: ys) = ?localZipWith_rhs_1
> 
> f x :: map f xs
> isElem2 x (y :: ys) with (_)
>   isElem2 x (y :: ys) | with_pat = ?isElem2_rhs
>   isElem3 x (x :: ys) | (Yes Refl) = ?isElem3_rhs_3
> 
>               [] => ?bar_1
>               (x :: ys) => ?bar_2
> 
> elemVoid1 Here impossible
> elemVoid1 (There _) impossible
> 
>                    Here impossible
>                    (There _) impossible
> 
interactive002 finished...FAILURE
0a1,10
> Nat
> Nat
> Nat
> Nat
> Vect (n + m) a
> Nat
> Nat
> (S n)
> String
> ()
interactive003 finished...FAILURE
0a1,5
> ys
> x :: app xs ys
> []
> f x y :: vzipWith f xs ys
> ?word_length_rhs_3 :: word_length xs
interactive004 finished...FAILURE
0a1,2
> plus ?foo_rhs2 ?foo_rhs3
> (append k m ?append_rhs2 ?append_rhs3)
interactive005 finished...FAILURE
0a1,36
> 3 : Nat
> Hello, World
> Main.main : IO ()
>     This is a docstring
>     
>     The function is Total
> Main.main is Total
> Hello, World
> id : a -> a
> Prelude.Basics.id : {a : Type} -> a -> a
> id : a -> a
> 
> 	 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY  
> 	 EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE     
> 	 IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR    
> 	 PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE   
> 	 LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR   
> 	 CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF  
> 	 SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR       
> 	 BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
> 	 WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE  
> 	 OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
> 	 IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
> 
> Main.main : IO ()
>     This
>     is a
>     docstring
>     
>     The function is Total
> Main.main : IO ()
>     This is a docstring
>     
>     The function is Total
> Nat2 : Type
> Invalid filename for compiler output "Test.idr"
interactive006 finished...FAILURE
0a1
> plus ?foo_rhs2 ?foo_rhs3
interactive007 finished...FAILURE
0a1
> Idris> *Data/ZZ> *Data/ZZ> *Data/ZZ> *Data/ZZ> Bye bye
interactive008 finished...FAILURE
0a1,204
> Idris> Idris> Idris> 1 ::
> 2 :: 3 :: 4 :: 5 :: ... : List Integer
> Idris> Idris> [1,
>  2,
>  3,
>  4,
>  5,
>  6,
>  7,
>  8,
>  9,
>  10,
>  11,
>  12,
>  13,
>  14,
>  15,
>  16,
>  17,
>  18,
>  19,
>  20,
>  21,
>  22,
>  23,
>  24,
>  25,
>  26,
>  27,
>  28,
>  29,
>  30,
>  31,
>  32,
>  33,
>  34,
>  35,
>  36,
>  37,
>  38,
>  39,
>  40,
>  41,
>  42,
>  43,
>  44,
>  45,
>  46,
>  47,
>  48,
>  49,
>  50,
>  51,
>  52,
>  53,
>  54,
>  55,
>  56,
>  57,
>  58,
>  59,
>  60,
>  61,
>  62,
>  63,
>  64,
>  65,
>  66,
>  67,
>  68,
>  69,
>  70,
>  71,
>  72,
>  73,
>  74,
>  75,
>  76,
>  77,
>  78,
>  79,
>  80,
>  81,
>  82,
>  83,
>  84,
>  85,
>  86,
>  87,
>  88,
>  89,
>  90,
>  91,
>  92,
>  93,
>  94,
>  95,
>  96,
>  97,
>  98,
>  99,
>  100] : List Integer
> Idris> Idris> ... : ...
> Idris> Idris> [1,
>  2,
>  3,
>  4,
>  5,
>  6,
>  7,
>  8,
>  9,
>  10,
>  11,
>  12,
>  13,
>  14,
>  15,
>  16,
>  17,
>  18,
>  19,
>  20,
>  21,
>  22,
>  23,
>  24,
>  25,
>  26,
>  27,
>  28,
>  29,
>  30,
>  31,
>  32,
>  33,
>  34,
>  35,
>  36,
>  37,
>  38,
>  39,
>  40,
>  41,
>  42,
>  43,
>  44,
>  45,
>  46,
>  47,
>  48,
>  49,
>  50,
>  51,
>  52,
>  53,
>  54,
>  55,
>  56,
>  57,
>  58,
>  59,
>  60,
>  61,
>  62,
>  63,
>  64,
>  65,
>  66,
>  67,
>  68,
>  69,
>  70,
>  71,
>  72,
>  73,
>  74,
>  75,
>  76,
>  77,
>  78,
>  79,
>  80,
>  81,
>  82,
>  83,
>  84,
>  85,
>  86,
>  87,
>  88,
>  89,
>  90,
>  91,
>  92,
>  93,
>  94,
>  95,
>  96,
>  97,
>  98,
>  99,
>  100] : List Integer
> Idris> Bye bye
interactive009 finished...FAILURE
0a1
> (IsSetCons pf prfRec)
interactive010 finished...FAILURE
0a1,20
> Prelude.List.(++) : List a -> List a -> List a
> Prelude.Strings.(++) : String -> String -> String
> a is not an implicit argument of Prelude.Interfaces./
> Usage is :doc <functionname>
> Usage is :wc <functionname>
> Usage is :printdef <functionname>
> pat {ty504} : Type u. pat {__class505} : Prelude.Interfaces.Fractional {ty504}. Prelude.Interfaces./ {ty504} {__class505}
> 
>  : pty {ty504} : Type u. pty {__class505} : Prelude.Interfaces.Fractional {ty504}. {ty504} -> {ty504} -> {ty504}
> (input):1:1: error: expected: ":",
>     dependent type signature,
>     end of input
> /<EOF> 
> ^      
> (input):1:1: error: expected: ":",
>     dependent type signature,
>     end of input
> ++<EOF> 
> ^       
> Can't find implementation for Fractional ty
interactive011 finished...FAILURE
0a1,3
>     show x = ?Show_rhs_1
>     showPrec d x = ?Show_rhs_2
> append [] _ = ?append_rhs_1
interactive012 finished...FAILURE
0a1,33
>   x : Int
> --------------------------------------
> mkString_rhs_1 : String
>   x : String
> --------------------------------------
> mkString_rhs_2 : String
> --------------------------------------
> mkThing_rhs_1 : Int
> --------------------------------------
> mkThing_rhs_2 : String
>   str : Bool
>   x : IntString str
> --------------------------------------
> mkString2_rhs : String
>   x : ?what
> --------------------------------------
> mkString3_rhs_1 : String
>   x : ?what
> --------------------------------------
> mkString3_rhs_2 : String
>   a : Type
>   m : Nat
>   ys : Vect m a
> --------------------------------------
> append_rhs_1 : Vect m a
>   a : Type
>   x : a
>   k : Nat
>   xs : Vect k a
>   m : Nat
>   ys : Vect m a
> --------------------------------------
> append_rhs_2 : Vect (S (plus k m)) a
io001 finished...FAILURE
0a1,16
> Reading testfile
> Hello!
> World!
> ...
> 3
> 4
> Last line
> 
> ---
> Hello!
> World!
> ...
> 3
> 4
> Last line
> ---
io002 finished...FAILURE
0a1,3
> First and second? 2
> 1
> 2
io003 finished...FAILURE
0a1,15
> Sending
> Hello!
> Received
> Hello to you too!
> Finished
> Sending
> Hello!
> Received
> Hello to you too!
> Finished
> Sending
> Hello!
> Received
> Hello to you too!
> Finished
literate001 finished...FAILURE
0a1,7
> ./test003a.lidr:1:0:Program line next to comment
> 'a'
> 'd'
> zabcdefg
> gfedcba
> ['g', 'f', 'e', 'd', 'c', 'b', 'a']
> abcdefg
meta001 finished...success
meta002 finished...FAILURE
0a1,10
> Tacs.idr:298:15:
> When checking right hand side of testElab3 with expected type
>         Sigma Ty (Tm [])
> 
> Unifying ty and ARR ty t would lead to infinite value
> AgdaStyleReflection.idr:328:5:
> When checking right hand side of baz with expected type
>         (Nat, Void)
> 
> PROOF SEARCH FAILURE is not defined.
meta003 finished...FAILURE
0a1,6
> BadDef.idr:12:1-9:
> While running an elaboration script, the following error occurred:
> Type mismatch between
>         ()
> and
>         String
meta004 finished...FAILURE
0a1,3
> meta004.idr:48:1-9:
> While running an elaboration script, the following error occurred:
> Not an impossible case
pkg001 finished...success
pkg002 finished...success
pkg003 finished...success
pkg004 finished...FAILURE
0a1,5
> Uncaught error: user error (test.ipkg:9:1: error: filename
>     must contain no directory
>     component, expected: space
> <EOF> 
> ^     )
primitives001 finished...FAILURE
0a1,27
> 8
> ("abc", "123")
> ("abc", "123")
> ([1, 2], [3, 4, 5])
> ([1, 2], [3, 4, 5])
> ello! here's the thing
> 22
> 0
> 用的依赖类
> Idris
> []
> is 是一个通用
> 8
> is 是一个通用的依赖类型纯函数式编程语言，其类型系统与 Agda 以及 Epigram 相似。
> 48
> Idris 是一个通用的依赖类型纯函
> 18
> 
> 0
> is is a 
> 8
> is is a general-purpose purely functional programming language with dependent types. 
> 85
> Idris is a general
> 18
> 
> 0
primitives002 finished...FAILURE
2c2
< missing primitive in 
---
> "0"
4c4
< missing primitive in 
---
> 0
6c6
< missing primitive in 
---
> 2
8c8
< missing primitive in 
---
> 0
10c10
< missing primitive in 
---
> 1
12c12
< missing primitive in 
---
> 1
14c14
< missing primitive in 
---
> 1
16c16
< missing primitive in 
---
> 0
18c18
< missing primitive in 
---
> 1
20c20
< missing primitive in 
---
> 0
22c22
< missing primitive in 
---
> 1
24c24
< missing primitive in 
---
> 0
26c26
< missing primitive in 
---
> 0.78539816
28c28
< missing primitive in 
---
> 0.54030230
30c30
< missing primitive in 
---
> 1
32c32
< missing primitive in 
---
> 0.84147098
34c34
< missing primitive in 
---
> 1.55740772
36c36
< missing primitive in 
---
> 1.57079632
38c38
< missing primitive in 
---
> 1
40c40
< missing primitive in 
---
> 2.71828182
42c42
< missing primitive in 
---
> 0
44c44
< missing primitive in 
---
> 1
46c46
< missing primitive in 
---
> -1
primitives003 finished...FAILURE
0a1,27
> True
> False
> True
> False
> True
> False
> True
> False
> True
> False
> False
> True
> False
> True
> True
> False
> True
> False
> False
> True
> False
> False
> False
> True
> False
> True
> False
proof001 finished...FAILURE
0a1,4
> test029.idr:29:25-30:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> test029.idr:36:25-30:
> This style of tactic proof is deprecated. See %runElab for the replacement.
proof002 finished...FAILURE
0a1,21
> Reflect.idr:174:21-26:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> Reflect.idr:183:21-26:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> Reflect.idr:191:15-20:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> test030a.idr:12:26-14:1:
> When checking right hand side of testReflect1 with expected type
>         ys ++ x :: ys ++ xs = (xs ++ [x]) ++ ys ++ xs
> 
> When checking an application of function Reflect.getJust:
>         Type mismatch between
>                 IsJust (Just x1) (Type of ItIsJust)
>         and
>                 IsJust (prove (getProof x)) (Expected type)
>         
>         Specifically:
>                 Type mismatch between
>                         Just x
>                 and
>                         Nothing
proof003 finished...FAILURE
0a1,15
> Parity.idr:17:18-23:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> Parity.idr:24:18-23:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> test015.idr:88:15-20:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> test015.idr:97:16-21:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> test015.idr:108:20-25:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> test015.idr:136:20-25:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> 00101010
> 01011001
> 010000011
proof004 finished...success
proof005 finished...success
proof006 finished...success
proof007 finished...FAILURE
0a1,6
> DefaultArgUnknownName.idr:9:6:
> When checking right hand side of test with expected type
>         ()
> 
> When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:
>         No such variable sadgjhsag
proof008 finished...FAILURE
0a1,2
> ClaimAndUnfocus.idr:8:27-32:
> This style of tactic proof is deprecated. See %runElab for the replacement.
proof009 finished...FAILURE
0a1,26
> Warning: this interactive prover is deprecated and will be removed in a future release. Please see :elab for a similar feature that will replace it.
> 
> 
> ----------                 Goal:                  ----------
> {hole0} : Int -> Int -> Int
> -Main.arhs> ----------              Other goals:              ----------
> {hole0}
> ----------              Assumptions:              ----------
>  x : Int
> ----------                 Goal:                  ----------
> {hole1} : Int -> Int
> -Main.arhs> ----------              Other goals:              ----------
> {hole1},{hole0}
> ----------              Assumptions:              ----------
>  x : Int
>  y : Int
> ----------                 Goal:                  ----------
> {hole2} : Int
> -Main.arhs> arhs: No more goals.
> -Main.arhs> Proof completed!
> Main.arhs = proof
>   intro x
>   intros
>   trivial
> 
> 
proof010 finished...FAILURE
0a1,6
> 2, << function >>
> 3, << function >>
> 
> some bools
> some bools
> 
proofsearch001 finished...success
proofsearch002 finished...success
proofsearch003 finished...success
pruviloj001 finished...success
quasiquote001 finished...FAILURE
0a1,5
> App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))))
> --------------
> App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1))))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1)))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))
> --------------
> App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))
quasiquote002 finished...FAILURE
0a1
> con
quasiquote003 finished...FAILURE
0a1,5
> NoInfer.idr:11:5:
> When checking right hand side of zzz with expected type
>         TT
> 
> No such variable k
quasiquote004 finished...FAILURE
0a1,11
> Quasiquote004.idr:39:26-31:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> Quasiquote004.idr:42:28-33:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> Quasiquote004.idr:50:27-32:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> Quasiquote004.idr:50:25:
> When checking right hand side of Quasiquote004.getMeNat' with expected type
>         String
> 
> Not a Nat goal
quasiquote005 finished...success
quasiquote006 finished...FAILURE
0a1,19
> quasiquote006.idr:9:3:
> When checking right hand side of b with expected type
>         TTName
> 
> Can't disambiguate name: ForeignEnv.Nil, 
>                          Prelude.List.Nil
> quasiquote006.idr:12:3:
> When checking right hand side of c with expected type
>         TTName
> 
> No such variable alsdkjflkj
> quasiquote006.idr:15:3:
> When checking right hand side of d with expected type
>         TTName
> 
> Can't disambiguate name: ForeignEnv.::, 
>                          Prelude.List.::, 
>                          Prelude.Stream.::
> quasiquote006.idr:17:3:Main.d already defined
records001 finished...FAILURE
0a1,5
> "foo"
> "Fred"
> [1, 2, 3]
> ["b", "a"]
> 25
records002 finished...FAILURE
0a1,2
> 42, 20
> 10, 42
records003 finished...FAILURE
0a1,6
> "Fred"
> 21
> 20
> 30
> 29
> 2014
records004 finished...FAILURE
0a1,3
> "Fred"
> "Joe"
> "Bloggs"
reg001 finished...success
reg002 finished...FAILURE
0a1
> [2, 1, 4, 3, 5]
reg003 finished...FAILURE
0a1,6
> reg003a.idr:4:11:When checking type of Main.ECons:
> No such variable OddList
> reg003a.idr:7:11:When checking type of Main.OCons:
> No such variable EvenList
> reg003a.idr:9:6:When checking type of Main.test:
> No such variable EvenList
reg004 finished...FAILURE
0a1,2
> 0
> 1
reg005 finished...FAILURE
0a1,3
> hey
> you
> [(), ()]
reg006 finished...FAILURE
0a1,2
> reg006.idr:17:1:
> RBTree.lookup is possibly not total due to: RBTree.case block in lookup at reg006.idr:19:8
reg007 finished...FAILURE
0a1,15
> reg007.lidr:8:1:A.n is already defined
> reg007.lidr:12:11-17:
> When checking right hand side of hurrah with expected type
>         0 = 1
> 
> Type mismatch between
>         n = lala (Type of isSame)
> and
>         0 = 1 (Expected type)
> 
> Specifically:
>         Type mismatch between
>                 1
>         and
>                 0
reg010 finished...FAILURE
0a1,3
> reg010.idr:5:15:
> When checking left hand side of with block in usubst.unsafeSubst:
> Can't match on with block in usubst.unsafeSubst warg a P x x px
reg013 finished...FAILURE
0a1,3
> 5
> 1
> 0
reg016 finished...FAILURE
0a1
> 429496729500000000000000
reg017 finished...FAILURE
0a1,5
> reg017.idr:5:17-24:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> reg017.idr:8:17-24:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> 4
reg018 finished...FAILURE
0a1,10
> reg018a.idr:16:1:
> conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat
> reg018a.idr:21:1:
> conat.loopForever is possibly not total due to: conat.minusCoNat
> reg018b.idr:8:1:
> A.showB is possibly not total due to recursive path A.showB
> reg018c.idr:21:1:
> CodataTest.inf is possibly not total due to: with block in CodataTest.inf
> reg018d.idr:8:1:
> Main.pull is not total as there are missing cases
reg020 finished...FAILURE
0a1,7
> length of: '' is: 0
> length of: 'hello world!' is: 12
> length of: ' ' is: 1
> length of: '	' is: 1
> length of: '
> ' is: 1
> length of all matches sum of all lengths: True
reg023 finished...FAILURE
0a1,8
> reg023.idr:7:5:
> When checking right hand side of bad with expected type
>         f Nat
> 
> Type mismatch between
>         Nat (Type of 0)
> and
>         f Nat (Expected type)
reg024 finished...FAILURE
0a1
> The answer is 42
reg025 finished...FAILURE
0a1
> l
reg027 finished...FAILURE
0a1,4
> <<int fn>>
> 6
> reg027a.idr:9:16:
> Overlapping implementation: Show (Int -> a) already defined
reg028 finished...FAILURE
0a1,6
> reg028.idr:5:1:
> tbad.bad is possibly not total due to: with block in tbad.bad
> reg028a.idr:17:14-19:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> reg028a.idr:11:1:
> tbad.qsort' is possibly not total due to: with block in tbad.qsort'
reg029 finished...FAILURE
0a1,4
> Nothing
> Just "exists!"
> Nothing
> Just "exists!"
reg031 finished...FAILURE
0a1
> [10, 128, 201, 255, 10, 51, 10, 52]
reg032 finished...FAILURE
0a1
> hello, world!
reg034 finished...FAILURE
0a1,4
> reg034.idr:6:5:When checking left hand side of bar:
> Can't match on bar xs xs Refl
> reg034.idr:9:5:When checking left hand side of foo:
> Can't match on foo f x x Refl
reg035 finished...FAILURE
0a1
> reg035b.idr:8:6:No such variable __pi_arg
reg036 finished...success
reg037 finished...success
reg038 finished...success
reg039 finished...FAILURE
0a1
> [3, 2, 1]
reg040 finished...FAILURE
0a1
> 42
reg041 finished...FAILURE
0a1,2
> ?prf : (x : Bool) -> (x1 : Bool) -> El (EQ Two x Two x1) -> El (EQ Two x Two x1)
> Z
reg042 finished...FAILURE
0a1
> 7
reg044 finished...FAILURE
0a1,16
> reg044.idr:4:6-11:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> reg044.idr:4:4:
> When checking right hand side of Main.pf with expected type
>         (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
> 
> Type mismatch between
>         b = b (Type of Refl)
> and
>         a = b (Expected type)
> 
> Specifically:
>         Type mismatch between
>                 b
>         and
>                 a
reg045 finished...FAILURE
0a1
> [1, 2, 3]
reg046 finished...success
reg047 finished...success
reg048 finished...success
reg049 finished...FAILURE
0a1,7
> reg049.idr:2:9:When checking constructor Main.Bogus:
> Void is not Main.Foo
> reg049.idr:5:6:
> When checking right hand side of uhOh with expected type
>         Void
> 
> No such variable Bogus
reg050 finished...FAILURE
0a1,10
> ./badbangop.idr:7:1: error: ! is
>     not a valid
>     operator, expected: space
> (!) : List a -> Nat -> Maybe a 
> ^                              
> ./baddoublebang.idr:6:28: error: unexpected
>     Operator without known fixity:
>     !!, expected: space
> doubleBang mmn = do pure !!mmn 
>                            ^   
reg052 finished...FAILURE
0a1
> 000000000000002A
reg053 finished...success
reg054 finished...FAILURE
0a1,13
> reg054.idr:18:5:When checking left hand side of inf:
> When checking an application of constructor Main.MkInfer:
>         Attempting concrete match on polymorphic argument: 0
> reg054.idr:34:7:When checking left hand side of weird:
> No explicit types on left hand side: Char
> reg054.idr:37:8:When checking left hand side of weird':
> No explicit types on left hand side: Nat
> reg054.idr:40:1-8:When checking left hand side of tctrick:
> When checking an application of Main.tctrick:
>         Type mismatch between
>                 Maybe a1 (Type of Just x)
>         and
>                 a (Expected type)
reg055 finished...FAILURE
0a1,9
> reg055.idr:5:3:When checking left hand side of g:
> Can't match on g (f 0)
> reg055.idr:8:3:When checking left hand side of h:
> Can't match on h x x
> reg055a.idr:8:5:When checking left hand side of foo:
> When checking an application of constructor Foo.CAny:
>         Attempting concrete match on polymorphic argument: Nothing
> reg055a.idr:13:7:When checking left hand side of Foo.apply:
> Can't match on apply (\x => \y => x) a
reg056 finished...FAILURE
0a1,2
> reg056.idr:7:7:dodgy n m Refl is a valid case
> reg056.idr:10:6:nonk Refl is a valid case
reg057 finished...success
reg058 finished...success
reg059 finished...success
reg060 finished...success
reg061 finished...success
reg062 finished...success
reg063 finished...success
reg064 finished...success
reg065 finished...success
reg066 finished...success
reg067 finished...FAILURE
0a1
> tst2["as"]
sourceLocation001 finished...FAILURE
0a1,19
> SourceLoc.idr:11:19-26:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> SourceLoc.idr:20:19-24:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> SourceLoc.idr:40:20-27:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> SourceLoc.idr:98:18-23:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> Testing using definition
> FileLoc "SourceLoc.idr" (16, 11) (16, 17)
> Testing using inline tactics
> FileLoc "SourceLoc.idr" (20, 17) (20, 17)
> Testing using metavariable with later definition
> FileLoc "SourceLoc.idr" (98, 16) (98, 16)
> -----------------------
> Success!
> Error at FileLoc "SourceLoc.idr" (72, 23) (72, 26)
> Success!
> Success!
sugar001 finished...FAILURE
0a1,4
> Just 8
> Just 9
> Just 42
> Nothing
sugar002 finished...FAILURE
0a1
> [(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50))]
sugar003 finished...FAILURE
0a1,12
> Counting:
> Number 1
> Number 2
> Number 3
> Number 4
> Number 5
> Number 6
> Number 7
> Number 8
> Number 9
> Number 10
> Done!
sugar004 finished...FAILURE
0a1,3
> No arguments!
> 42
> Too many arguments!
sugar005 finished...FAILURE
0a1,9
> Nothing
> Just 1
> Nothing
> Just 1
> Just (5, 4)
> Nothing
> Just 2
> Just 42
> Nothing
syntax001 finished...FAILURE
0a1,18
> Syntax.idr:6:7-9:1:
> When checking right hand side of foo with expected type
>         Nat
> 
> When checking an application of function Prelude.Interfaces.+:
>         Type mismatch between
>                 String (Type of "argh")
>         and
>                 Nat (Expected type)
> SyntaxTest.idr:5:7-6:1:
> When checking right hand side of foo with expected type
>         Nat
> 
> When checking an application of function Prelude.Interfaces.+:
>         Type mismatch between
>                 String (Type of "argh")
>         and
>                 Nat (Expected type)
syntax002 finished...FAILURE
0a1,2
> Nothing
> 7
tactics001 finished...success
totality001 finished...FAILURE
0a1,6
> test010.idr:15:1:
> Main.foo is possibly not total due to: Main.MkBad
> test010a.idr:9:1:
> main.bar is possibly not total due to: main.MkBad
> test010b.idr:9:1:
> main.bar is possibly not total due to: main.MkBad
totality002 finished...FAILURE
0a1,6
> test017.idr:94:26-31:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> test017a.idr:7:1:
> scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans
> test017b.idr:4:1:
> foo.foo is possibly not total due to recursive path foo.foo
totality003 finished...FAILURE
0a1,2
> totality003a.idr:5:1:
> smaller.qsort is possibly not total due to recursive path smaller.qsort --> smaller.qsort --> smaller.qsort
totality004 finished...FAILURE
0a1,5
> [1, 2, 2, 4, 3, 6, 4, 8, 5, 10]
> totality004a.idr:13:1:
> Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process
> totality004a.idr:24:1:
> Main.main is possibly not total due to: Main.process
totality005 finished...FAILURE
0a1
> [0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377]
totality006 finished...FAILURE
0a1,5
> totality006.idr:8:1:
> Main.prf is not total as there are missing cases
> totality006a.idr:11:6:prf' (S _) (S _) Oh is a valid case
> totality006b.idr:10:1:
> totality006b.blargh is not total as there are missing cases
totality007 finished...FAILURE
0a1,5
> Entering directory `./src'
> Totality.idr:4:1:
> Totality.foo is not total as there are missing cases
> Totality.idr:4:1:Could not build: Totality.foo is not total as there are missing cases
> Leaving directory `./src'
totality008 finished...FAILURE
0a1,2
> totality008.idr:7:1:
> Main.ElimT is possibly not total due to: Main.C2
totality009 finished...FAILURE
0a1,8
> TestLambdaPossible.idr:9:25:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25 is not total as there are missing cases
> TestLambdaPossible.idr:9:1:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25
> TestLambdaPossible.idr:12:25:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases
> TestLambdaPossible.idr:12:1:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25
> TestLambdaPossible.idr:9:15:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25 is not total as there are missing cases
> TestLambdaPossible.idr:9:1:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25
> TestLambdaPossible.idr:12:16:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases
> TestLambdaPossible.idr:12:1:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25
totality010 finished...FAILURE
0a1,4
> totality010.idr:27:1:
> Main.evenNotS is not total as there are missing cases
> totality010.idr:30:1:
> Main.bad is possibly not total due to: Main.evenNotS
tutorial001 finished...success
tutorial002 finished...FAILURE
0a1,6
> tutorial002.idr:41:25-30:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> tutorial002.idr:48:18-23:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> tutorial002.idr:54:18-23:
> This style of tactic proof is deprecated. See %runElab for the replacement.
tutorial003 finished...success
tutorial004 finished...FAILURE
0a1,4
> tutorial004.idr:46:14-19:
> This style of tactic proof is deprecated. See %runElab for the replacement.
> tutorial004.idr:53:14-19:
> This style of tactic proof is deprecated. See %runElab for the replacement.
tutorial005 finished...success
tutorial006 finished...FAILURE
0a1,29
> tutorial006a.idr:5:23-25:
> When checking right hand side of vapp with expected type
>         Vect (S k + m) a
> 
> When checking argument xs to constructor Data.Vect.:::
>         Type mismatch between
>                 Vect (k + k) a (Type of vapp xs xs)
>         and
>                 Vect (plus k m) a (Expected type)
>         
>         Specifically:
>                 Type mismatch between
>                         plus k k
>                 and
>                         plus k m
> tutorial006b.idr:10:10:
> When checking right hand side of with block in Main.parity with expected type
>         Parity (S (S (j + j)))
> 
> Type mismatch between
>         Parity (plus (S j) (S j)) (Type of Even)
> and
>         Parity (S (S (plus j j))) (Expected type)
> 
> Specifically:
>         Type mismatch between
>                 plus (S j) (S j)
>         and
>                 S (S (plus j j))
unique001 finished...FAILURE
0a1,21
> 19,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END
> 19,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END
> 38,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END
> 38,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END
> unique001a.idr:33:11:Type mismatch between
>         Int -> String
> and
>         UniqueType (Int -> String)
> unique001a.idr:44:12:Type mismatch between
>         Int -> String
> and
>         UniqueType (Int -> String)
> unique001a.idr:55:12:Type mismatch between
>         UniqueType (Int -> String)
> and
>         Int -> String
> unique001b.idr:16:7:Borrowed name xs must not be used on RHS
> unique001c.idr:46:6:Unique name f is used more than once
> unique001d.idr:3:7:Borrowed name x must not be used on RHS
> unique001e.idr:3:10:
> Constructor Main.Nil has a UniqueType, but the data type does not
unique002 finished...FAILURE
0a1,5
> unique002.idr:15:5:Unique name xs is used more than once
> unique002a.idr:15:5:Type mismatch between
>         Int -> String
> and
>         UniqueType (Int -> String)
unique003 finished...FAILURE
0a1,4
> unique003.idr:18:5:Type mismatch between
>         Int -> String
> and
>         UniqueType (Int -> String)

----
192 tests run: 39 succesful, 153 failed, 0 updated.

Failed tests:
basic001
basic002
basic003
basic004
basic005
basic006
basic007
basic008
basic009
basic010
basic011
basic012
basic013
basic015
basic016
basic017
bignum001
bignum002
bounded001
classes001
corecords001
corecords002
delab001
docs001
docs002
docs003
docs004
dsl001
dsl002
dsl003
effects001
effects002
effects003
effects004
effects005
error001
error003
error004
error005
error006
ffi001
ffi002
ffi003
ffi005
ffi006
folding001
idrisdoc001
idrisdoc002
idrisdoc003
idrisdoc004
idrisdoc005
idrisdoc006
idrisdoc007
idrisdoc008
idrisdoc009
interactive001
interactive002
interactive003
interactive004
interactive005
interactive006
interactive007
interactive008
interactive009
interactive010
interactive011
interactive012
io001
io002
io003
literate001
meta002
meta003
meta004
pkg004
primitives001
primitives002
primitives003
proof001
proof002
proof003
proof007
proof008
proof009
proof010
quasiquote001
quasiquote002
quasiquote003
quasiquote004
quasiquote006
records001
records002
records003
records004
reg002
reg003
reg004
reg005
reg006
reg007
reg010
reg013
reg016
reg017
reg018
reg020
reg023
reg024
reg025
reg027
reg028
reg029
reg031
reg032
reg034
reg035
reg039
reg040
reg041
reg042
reg044
reg045
reg049
reg050
reg052
reg054
reg055
reg056
reg067
sourceLocation001
sugar001
sugar002
sugar003
sugar004
sugar005
syntax001
syntax002
totality001
totality002
totality003
totality004
totality005
totality006
totality007
totality008
totality009
totality010
tutorial002
tutorial004
tutorial006
unique001
unique002
unique003

Test suite regression-and-sanity-tests: FAIL
Test suite logged to: dist/test/idris-0.10-regression-and-sanity-tests.log
0 of 1 test suites (0 of 1 test cases) passed.