Skip to content

Instantly share code, notes, and snippets.

@ilovezfs
Created June 3, 2018 09:47
Show Gist options
  • Save ilovezfs/769d0c6a083a567f33865f601afda146 to your computer and use it in GitHub Desktop.
Save ilovezfs/769d0c6a083a567f33865f601afda146 to your computer and use it in GitHub Desktop.
==> /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