Created
June 3, 2018 09:47
-
-
Save ilovezfs/769d0c6a083a567f33865f601afda146 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
==> /usr/local/Cellar/agda/2.5.4/bin/agda -i . -i src --html --vim README.agda | |
Checking README (/usr/local/Cellar/agda/2.5.4/lib/agda/README.agda). | |
Checking Data.Bool (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Bool.agda). | |
Checking Relation.Nullary (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Nullary.agda). | |
Checking Data.Empty (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Empty.agda). | |
Checking Level (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Level.agda). | |
Checking Data.Empty.Irrelevant (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Empty/Irrelevant.agda). | |
Checking Relation.Binary (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary.agda). | |
Checking Data.Product (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Product.agda). | |
Checking Function (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Function.agda). | |
Checking Strict (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Strict.agda). | |
Checking Agda.Builtin.Equality (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/Equality.agda). | |
Checking Agda.Builtin.Strict (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/Strict.agda). | |
Checking Data.Sum (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Sum.agda). | |
Checking Data.Unit.Base (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Unit/Base.agda). | |
Checking Agda.Builtin.Unit (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/Unit.agda). | |
Checking Data.Maybe.Base (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Maybe/Base.agda). | |
Checking Data.Bool.Base (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Bool/Base.agda). | |
Checking Relation.Binary.Core (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/Core.agda). | |
Checking Data.Sum.Base (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Sum/Base.agda). | |
Checking Agda.Builtin.Bool (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/Bool.agda). | |
Checking Relation.Binary.PropositionalEquality.Core (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/PropositionalEquality/Core.agda). | |
Checking Relation.Binary.Consequences (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/Consequences.agda). | |
Checking Relation.Unary (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Unary.agda). | |
Checking Relation.Binary.Indexed.Core (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/Indexed/Core.agda). | |
Checking Relation.Binary.PropositionalEquality (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/PropositionalEquality.agda). | |
Checking Function.Equality (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Function/Equality.agda). | |
Checking Relation.Binary.Indexed (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/Indexed.agda). | |
Checking Relation.Binary.HeterogeneousEquality.Core (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/HeterogeneousEquality/Core.agda). | |
Checking Data.Char (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Char.agda). | |
Checking Data.Nat.Base (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Nat/Base.agda). | |
Checking Relation.Binary.PropositionalEquality.TrustMe (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/PropositionalEquality/TrustMe.agda). | |
Checking Agda.Builtin.TrustMe (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/TrustMe.agda). | |
Checking Agda.Builtin.Nat (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/Nat.agda). | |
Checking Data.Nat.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Nat/Properties.agda). | |
Checking Function.Injection (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Function/Injection.agda). | |
Checking Algebra (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra.agda). | |
Checking Algebra.FunctionProperties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/FunctionProperties.agda). | |
Checking Algebra.FunctionProperties.Core (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/FunctionProperties/Core.agda). | |
Checking Algebra.Structures (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/Structures.agda). | |
Checking Algebra.FunctionProperties.Consequences (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/FunctionProperties/Consequences.agda). | |
Checking Relation.Binary.EqReasoning (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/EqReasoning.agda). | |
Checking Relation.Binary.PreorderReasoning (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/PreorderReasoning.agda). | |
Checking Algebra.RingSolver.Simple (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/RingSolver/Simple.agda). | |
Checking Algebra.RingSolver.AlmostCommutativeRing (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/RingSolver/AlmostCommutativeRing.agda). | |
Checking Algebra.Morphism (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/Morphism.agda). | |
Checking Algebra.Properties.Group (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/Properties/Group.agda). | |
Checking Algebra.Properties.Ring (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/Properties/Ring.agda). | |
Checking Algebra.Properties.AbelianGroup (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/Properties/AbelianGroup.agda). | |
Checking Algebra.RingSolver (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/RingSolver.agda). | |
Checking Algebra.RingSolver.Lemmas (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/RingSolver/Lemmas.agda). | |
Checking Algebra.Operations.Semiring (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/Operations/Semiring.agda). | |
Checking Algebra.Operations.CommutativeMonoid (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/Operations/CommutativeMonoid.agda). | |
Checking Data.List (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List.agda). | |
Checking Data.List.Base (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Base.agda). | |
Checking Data.Fin (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Fin.agda). | |
Checking Data.Nat (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Nat.agda). | |
Checking Relation.Nullary.Decidable (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Nullary/Decidable.agda). | |
Checking Data.Unit (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Unit.agda). | |
Checking Function.Equivalence (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Function/Equivalence.agda). | |
Checking Relation.Unary.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Unary/Properties.agda). | |
Checking Relation.Nullary.Product (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Nullary/Product.agda). | |
Checking Relation.Nullary.Sum (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Nullary/Sum.agda). | |
Checking Relation.Nullary.Negation (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Nullary/Negation.agda). | |
Checking Category.Monad (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Category/Monad.agda). | |
Checking Category.Monad.Indexed (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Category/Monad/Indexed.agda). | |
Checking Category.Applicative.Indexed (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Category/Applicative/Indexed.agda). | |
Checking Category.Functor (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Category/Functor.agda). | |
Checking Agda.Builtin.List (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/List.agda). | |
Checking Data.Table.Base (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Table/Base.agda). | |
Checking Relation.Binary.Reflection (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/Reflection.agda). | |
Checking Data.Vec (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Vec.agda). | |
Checking Data.Vec.N-ary (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Vec/N-ary.agda). | |
Checking Relation.Binary.PartialOrderReasoning (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/PartialOrderReasoning.agda). | |
Checking Relation.Binary.On (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/On.agda). | |
Checking Agda.Builtin.Char (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/Char.agda). | |
Checking Data.String.Base (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/String/Base.agda). | |
Checking Data.Char.Core (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Char/Core.agda). | |
Checking Agda.Builtin.String (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/String.agda). | |
Checking Data.Char.Base (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Char/Base.agda). | |
Checking Data.Maybe (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Maybe.agda). | |
Checking Category.Monad.Identity (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Category/Monad/Identity.agda). | |
Checking Data.Stream (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Stream.agda). | |
Checking Coinduction (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Coinduction.agda). | |
Checking Agda.Builtin.Coinduction (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/Coinduction.agda). | |
Checking Data.Colist (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Colist.agda). | |
Checking Data.BoundedVec.Inefficient (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/BoundedVec/Inefficient.agda). | |
Checking Data.Conat (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Conat.agda). | |
Checking Data.List.NonEmpty (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/NonEmpty.agda). | |
Checking Data.Bool.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Bool/Properties.agda). | |
Checking Algebra.Properties.BooleanAlgebra (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/Properties/BooleanAlgebra.agda). | |
Checking Algebra.Properties.DistributiveLattice (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/Properties/DistributiveLattice.agda). | |
Checking Algebra.Properties.Lattice (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/Properties/Lattice.agda). | |
Checking Relation.Binary.Lattice (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/Lattice.agda). | |
Checking Function.Inverse (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Function/Inverse.agda). | |
Checking Function.Bijection (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Function/Bijection.agda). | |
Checking Function.Surjection (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Function/Surjection.agda). | |
Checking Function.LeftInverse (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Function/LeftInverse.agda). | |
Checking Relation.Binary.InducedPreorders (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/InducedPreorders.agda). | |
Checking Data.String (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/String.agda). | |
Checking Data.List.Relation.Lex.Strict (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Relation/Lex/Strict.agda). | |
Checking Data.List.Relation.Pointwise (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Relation/Pointwise.agda). | |
Checking Data.List.Relation.Lex.Core (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Relation/Lex/Core.agda). | |
Checking Category.Applicative (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Category/Applicative.agda). | |
Checking Induction (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Induction.agda). | |
Checking Induction.WellFounded (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Induction/WellFounded.agda). | |
Checking Induction.Nat (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Induction/Nat.agda). | |
Checking Data.Fin.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Fin/Properties.agda). | |
Checking IO (/usr/local/Cellar/agda/2.5.4/lib/agda/src/IO.agda). | |
Checking IO.Primitive (/usr/local/Cellar/agda/2.5.4/lib/agda/src/IO/Primitive.agda). | |
Checking Foreign.Haskell (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Foreign/Haskell.agda). | |
Checking Agda.Builtin.IO (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/IO.agda). | |
Checking README.Nat (/usr/local/Cellar/agda/2.5.4/lib/agda/README/Nat.agda). | |
Checking README.Integer (/usr/local/Cellar/agda/2.5.4/lib/agda/README/Integer.agda). | |
Checking Data.Integer (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Integer.agda). | |
Checking Data.Nat.Show (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Nat/Show.agda). | |
Checking Data.Digit (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Digit.agda). | |
Checking Data.Nat.DivMod (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Nat/DivMod.agda). | |
Checking Data.Sign (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Sign.agda). | |
Checking Data.Integer.Base (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Integer/Base.agda). | |
Checking Agda.Builtin.Int (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/Int.agda). | |
Checking Data.Integer.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Integer/Properties.agda). | |
Checking Data.Sign.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Sign/Properties.agda). | |
Checking README.AVL (/usr/local/Cellar/agda/2.5.4/lib/agda/README/AVL.agda). | |
Checking Data.AVL (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/AVL.agda). | |
Checking Data.DifferenceList (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/DifferenceList.agda). | |
Checking Data.AVL.Indexed (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/AVL/Indexed.agda). | |
Checking Data.AVL.Key (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/AVL/Key.agda). | |
Checking Data.AVL.Height (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/AVL/Height.agda). | |
Checking Data.AVL.IndexedMap (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/AVL/IndexedMap.agda). | |
Checking Data.AVL.Sets (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/AVL/Sets.agda). | |
Checking README.Record (/usr/local/Cellar/agda/2.5.4/lib/agda/README/Record.agda). | |
Checking Record (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Record.agda). | |
Checking README.Case (/usr/local/Cellar/agda/2.5.4/lib/agda/README/Case.agda). | |
Checking README.Container.FreeMonad (/usr/local/Cellar/agda/2.5.4/lib/agda/README/Container/FreeMonad.agda). | |
Checking Data.Container (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Container.agda). | |
Checking Data.M (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/M.agda). | |
Checking Data.W (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/W.agda). | |
Checking Function.Related (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Function/Related.agda). | |
Checking Data.Container.Combinator (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Container/Combinator.agda). | |
Checking Data.Container.FreeMonad (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Container/FreeMonad.agda). | |
Checking README.Function.Reasoning (/usr/local/Cellar/agda/2.5.4/lib/agda/README/Function/Reasoning.agda). | |
Checking Function.Reasoning (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Function/Reasoning.agda). | |
Checking Everything (/usr/local/Cellar/agda/2.5.4/lib/agda/Everything.agda). | |
Checking Algebra.CommutativeMonoidSolver (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/CommutativeMonoidSolver.agda). | |
Checking Data.Nat.GeneralisedArithmetic (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Nat/GeneralisedArithmetic.agda). | |
Checking Data.Vec.Relation.Pointwise.Inductive (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Vec/Relation/Pointwise/Inductive.agda). | |
Checking Data.Vec.All (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Vec/All.agda). | |
Checking Algebra.CommutativeMonoidSolver.Example (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/CommutativeMonoidSolver/Example.agda). | |
Checking Algebra.IdempotentCommutativeMonoidSolver (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/IdempotentCommutativeMonoidSolver.agda). | |
Checking Algebra.IdempotentCommutativeMonoidSolver.Example (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/IdempotentCommutativeMonoidSolver/Example.agda). | |
Checking Algebra.Monoid-solver (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/Monoid-solver.agda). | |
Checking Data.List.Relation.Equality.DecPropositional (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Relation/Equality/DecPropositional.agda). | |
Checking Data.List.Relation.Equality.Propositional (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Relation/Equality/Propositional.agda). | |
Checking Data.List.Relation.Equality.Setoid (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Relation/Equality/Setoid.agda). | |
Checking Data.List.Relation.Equality.DecSetoid (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Relation/Equality/DecSetoid.agda). | |
Checking Algebra.Properties.BooleanAlgebra.Expression (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/Properties/BooleanAlgebra/Expression.agda). | |
Checking Data.Vec.Categorical (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Vec/Categorical.agda). | |
Checking Category.Functor.Identity (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Category/Functor/Identity.agda). | |
Checking Data.Vec.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Vec/Properties.agda). | |
Checking Data.List.Any (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Any.agda). | |
Checking Data.List.Membership.Propositional (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Membership/Propositional.agda). | |
Checking Data.List.Membership.Setoid (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Membership/Setoid.agda). | |
Checking Relation.Binary.HeterogeneousEquality (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/HeterogeneousEquality.agda). | |
Checking Data.Unit.NonEta (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Unit/NonEta.agda). | |
Checking Data.Vec.Relation.Pointwise.Extensional (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Vec/Relation/Pointwise/Extensional.agda). | |
Checking Relation.Binary.Closure.Transitive (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/Closure/Transitive.agda). | |
Checking Algebra.RingSolver.Natural-coefficients (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Algebra/RingSolver/Natural-coefficients.agda). | |
Checking Category.Applicative.Predicate (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Category/Applicative/Predicate.agda). | |
Checking Category.Functor.Predicate (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Category/Functor/Predicate.agda). | |
Checking Relation.Unary.PredicateTransformer (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Unary/PredicateTransformer.agda). | |
Checking Category.Monad.Continuation (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Category/Monad/Continuation.agda). | |
Checking Category.Monad.Partiality (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Category/Monad/Partiality.agda). | |
Checking Category.Monad.Partiality.All (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Category/Monad/Partiality/All.agda). | |
Checking Category.Monad.Predicate (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Category/Monad/Predicate.agda). | |
Checking Category.Monad.State (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Category/Monad/State.agda). | |
Checking Data.Bin (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Bin.agda). | |
Checking Data.Bin.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Bin/Properties.agda). | |
Checking Data.List.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Properties.agda). | |
Checking Data.List.All (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/All.agda). | |
Checking Data.Bool.Show (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Bool/Show.agda). | |
Checking Data.BoundedVec (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/BoundedVec.agda). | |
Checking Data.Cofin (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Cofin.agda). | |
Checking Data.Colist.Infinite-merge (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Colist/Infinite-merge.agda). | |
Checking Data.Sum.Relation.Pointwise (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Sum/Relation/Pointwise.agda). | |
Checking Data.Sum.Relation.Core (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Sum/Relation/Core.agda). | |
Checking Function.Related.TypeIsomorphisms (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Function/Related/TypeIsomorphisms.agda). | |
Checking Data.Product.Relation.Pointwise.NonDependent (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Product/Relation/Pointwise/NonDependent.agda). | |
Checking Data.Product.Relation.Pointwise.Dependent (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Product/Relation/Pointwise/Dependent.agda). | |
Checking Data.Sum.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Sum/Properties.agda). | |
Checking Data.Container.Any (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Container/Any.agda). | |
Checking Data.Container.Indexed (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Container/Indexed.agda). | |
Checking Data.W.Indexed (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/W/Indexed.agda). | |
Checking Data.Container.Indexed.Core (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Container/Indexed/Core.agda). | |
Checking Data.M.Indexed (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/M/Indexed.agda). | |
Checking Data.Container.Indexed.Combinator (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Container/Indexed/Combinator.agda). | |
Checking Data.Container.Indexed.FreeMonad (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Container/Indexed/FreeMonad.agda). | |
Checking Data.Covec (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Covec.agda). | |
Checking Data.DifferenceNat (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/DifferenceNat.agda). | |
Checking Data.DifferenceVec (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/DifferenceVec.agda). | |
Checking Data.Fin.Dec (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Fin/Dec.agda). | |
Checking Data.Vec.Relation.Equality.DecPropositional (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Vec/Relation/Equality/DecPropositional.agda). | |
Checking Data.Vec.Relation.Equality.Propositional (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Vec/Relation/Equality/Propositional.agda). | |
Checking Data.Vec.Relation.Equality.Setoid (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Vec/Relation/Equality/Setoid.agda). | |
Checking Data.Vec.Relation.Equality.DecSetoid (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Vec/Relation/Equality/DecSetoid.agda). | |
Checking Data.Fin.Subset (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Fin/Subset.agda). | |
Checking Data.Fin.Subset.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Fin/Subset/Properties.agda). | |
Checking Data.Fin.Permutation (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Fin/Permutation.agda). | |
Checking Data.Fin.Permutation.Components (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Fin/Permutation/Components.agda). | |
Checking Data.Fin.Substitution (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Fin/Substitution.agda). | |
Checking Relation.Binary.Closure.ReflexiveTransitive (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/Closure/ReflexiveTransitive.agda). | |
Checking Data.Fin.Substitution.Example (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Fin/Substitution/Example.agda). | |
Checking Data.Fin.Substitution.Lemmas (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Fin/Substitution/Lemmas.agda). | |
Checking Data.Fin.Substitution.List (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Fin/Substitution/List.agda). | |
Checking Data.Float (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Float.agda). | |
Checking Agda.Builtin.Float (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/Float.agda). | |
Checking Data.Graph.Acyclic (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Graph/Acyclic.agda). | |
Checking Data.Integer.Addition.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Integer/Addition/Properties.agda). | |
Checking Data.Integer.Divisibility (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Integer/Divisibility.agda). | |
Checking Data.Nat.Divisibility (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Nat/Divisibility.agda). | |
Checking Data.Nat.Coprimality (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Nat/Coprimality.agda). | |
Checking Data.Nat.Primality (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Nat/Primality.agda). | |
Checking Data.Nat.GCD (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Nat/GCD.agda). | |
Checking Induction.Lexicographic (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Induction/Lexicographic.agda). | |
Checking Data.Nat.GCD.Lemmas (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Nat/GCD/Lemmas.agda). | |
Checking Data.Integer.Multiplication.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Integer/Multiplication/Properties.agda). | |
Checking Data.List.All.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/All/Properties.agda). | |
Checking Data.List.Relation.Sublist.Propositional (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Relation/Sublist/Propositional.agda). | |
Checking Data.List.Relation.Sublist.Setoid (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Relation/Sublist/Setoid.agda). | |
Checking Data.List.Any.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Any/Properties.agda). | |
Checking Data.List.Categorical (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Categorical.agda). | |
Checking Data.List.Membership.Propositional.Properties.Core (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Membership/Propositional/Properties/Core.agda). | |
Checking Data.Product.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Product/Properties.agda). | |
Checking Data.List.Membership.Setoid.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Membership/Setoid/Properties.agda). | |
Checking Data.List.Countdown (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Countdown.agda). | |
Checking Data.List.Membership.DecPropositional (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Membership/DecPropositional.agda). | |
Checking Data.List.Membership.DecSetoid (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Membership/DecSetoid.agda). | |
Checking Data.List.Membership.Propositional.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Membership/Propositional/Properties.agda). | |
Checking Relation.Binary.Properties.DecTotalOrder (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/Properties/DecTotalOrder.agda). | |
Checking Relation.Binary.NonStrictToStrict (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/NonStrictToStrict.agda). | |
Checking Data.List.NonEmpty.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/NonEmpty/Properties.agda). | |
Checking Data.List.Relation.BagAndSetEquality (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Relation/BagAndSetEquality.agda). | |
Checking Data.List.Relation.Sublist.Propositional.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Relation/Sublist/Propositional/Properties.agda). | |
Checking Data.List.Relation.Sublist.Setoid.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Relation/Sublist/Setoid/Properties.agda). | |
Checking Data.List.Relation.Lex.NonStrict (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Relation/Lex/NonStrict.agda). | |
Checking Data.List.Reverse (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Reverse.agda). | |
Checking Data.List.Zipper (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Zipper.agda). | |
Checking Data.List.Zipper.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/List/Zipper/Properties.agda). | |
Checking Data.Nat.InfinitelyOften (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Nat/InfinitelyOften.agda). | |
Checking Data.Nat.LCM (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Nat/LCM.agda). | |
Checking Data.Nat.Properties.Simple (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Nat/Properties/Simple.agda). | |
Checking Data.Plus (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Plus.agda). | |
Checking Data.Product.N-ary (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Product/N-ary.agda). | |
Checking Data.Product.N-ary.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Product/N-ary/Properties.agda). | |
Checking Data.Product.Relation.Lex.NonStrict (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Product/Relation/Lex/NonStrict.agda). | |
Checking Data.Product.Relation.Lex.Strict (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Product/Relation/Lex/Strict.agda). | |
Checking Data.Rational (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Rational.agda). | |
Checking Data.Rational.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Rational/Properties.agda). | |
Checking Data.ReflexiveClosure (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/ReflexiveClosure.agda). | |
Checking Relation.Binary.Closure.Reflexive (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/Closure/Reflexive.agda). | |
Checking Relation.Binary.Simple (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/Simple.agda). | |
Checking Data.Star (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Star.agda). | |
Checking Data.Star.BoundedVec (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Star/BoundedVec.agda). | |
Checking Data.Star.Nat (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Star/Nat.agda). | |
Checking Data.Star.Decoration (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Star/Decoration.agda). | |
Checking Data.Star.Pointer (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Star/Pointer.agda). | |
Checking Data.Star.List (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Star/List.agda). | |
Checking Data.Star.Environment (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Star/Environment.agda). | |
Checking Data.Star.Fin (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Star/Fin.agda). | |
Checking Data.Star.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Star/Properties.agda). | |
Checking Relation.Binary.Closure.ReflexiveTransitive.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Relation/Binary/Closure/ReflexiveTransitive/Properties.agda). | |
Checking Data.Star.Vec (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Star/Vec.agda). | |
Checking Data.Sum.Relation.LeftOrder (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Sum/Relation/LeftOrder.agda). | |
Checking Data.Table (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Table.agda). | |
Checking Data.Table.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Table/Properties.agda). | |
Checking Data.Table.Relation.Equality (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Table/Relation/Equality.agda). | |
Checking Data.Vec.All.Properties (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Data/Vec/All/Properties.agda). | |
Checking Reflection (/usr/local/Cellar/agda/2.5.4/lib/agda/src/Reflection.agda). | |
Checking Agda.Builtin.Reflection (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/Reflection.agda). | |
Checking Agda.Builtin.Word (/usr/local/Cellar/agda/2.5.4/share/x86_64-osx-ghc-8.4.3/Agda-2.5.4/lib/prim/Agda/Builtin/Word.agda). | |
/usr/local/Cellar/agda/2.5.4/lib/agda/src/Reflection.agda:139,1-144,21 | |
Incomplete pattern matching for showLiteral. Missing cases: | |
showLiteral (Literal.word64 n) | |
when checking the definition of showLiteral | |
/usr/local/Cellar/agda/2.5.4/lib/agda/src/Reflection.agda:328,1-363,21 | |
Incomplete pattern matching for _≟-Lit_. Missing cases: | |
Literal.word64 n ≟-Lit nat n₁ | |
x ≟-Lit Literal.word64 n | |
Literal.word64 n ≟-Lit float x | |
Literal.word64 n ≟-Lit char c | |
Literal.word64 n ≟-Lit string s | |
Literal.word64 n ≟-Lit name x | |
Literal.word64 n ≟-Lit meta x | |
when checking the definition of _≟-Lit_ | |
/usr/local/Homebrew/Library/Homebrew/debrew.rb:11:in `raise' |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment