Agda: Failed to install agda on OS X

Created on 22 Feb 2021  路  3Comments  路  Source: agda/agda

I followed the OS X instructions to try and install Agda on my Big Sur Mac using brew. However, I get:

$ cat hello-world.agda
module hello-world where

open import IO

main = run (putStrLn "Hello, World!")
$ agda --compile hello-world.agda
Checking hello-world (/Users/satnam/agda-examples/hello-world.agda).
Unsolved metas at the following locations:
  /Users/satnam/agda-examples/hello-world.agda:5,8-11

More details:

$ agda --version
Agda version 2.6.1.3
$ cat ~/.agda/default
standard-library

Any idea about what I did wrong? Many thanks.

Most helpful comment

Thank you. That works! Now I can start to actually try and learn some Agda!
I was not expecting this to actually build the world :-)

$ agda --compile hello-world.agda
Checking hello-world (/Users/satnam/agda-examples/hello-world.agda).
Compiling Agda.Primitive in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Primitive.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Primitive.hs
Compiling Agda.Builtin.Equality in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Equality.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Equality.hs
Compiling Data.Empty in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Empty.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Empty.hs
Compiling Data.Empty.Irrelevant in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Empty/Irrelevant.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Empty/Irrelevant.hs
Compiling Agda.Builtin.Bool in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Bool.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Bool.hs
Compiling Agda.Builtin.Unit in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Unit.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Unit.hs
Compiling Data.Unit.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Unit/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Unit/Base.hs
Compiling Level in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Level.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Level.hs
Compiling Data.Bool.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Bool/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Bool/Base.hs
Compiling Relation.Nullary in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary.hs
Compiling Relation.Nullary.Reflects in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary/Reflects.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary/Reflects.hs
Compiling Agda.Builtin.Strict in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Strict.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Strict.hs
Compiling Strict in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Strict.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Strict.hs
Compiling Function.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Base.hs
Compiling Data.Sum.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Sum/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Sum/Base.hs
Compiling Data.These.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/These/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/These/Base.hs
Compiling Agda.Builtin.Sigma in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Sigma.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Sigma.hs
Compiling Data.Product in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Product.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Product.hs
Compiling Data.Maybe.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Maybe/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Maybe/Base.hs
Compiling Relation.Binary.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Core.hs
Compiling Relation.Binary.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Definitions.hs
Compiling Relation.Binary.PropositionalEquality.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/PropositionalEquality/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/PropositionalEquality/Core.hs
Compiling Relation.Nullary.Decidable.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary/Decidable/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary/Decidable/Core.hs
Compiling Relation.Unary in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Unary.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Unary.hs
Compiling Relation.Binary.Consequences in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Consequences.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Consequences.hs
Compiling Relation.Binary.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Structures.hs
Compiling Relation.Binary.Bundles in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Bundles.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Bundles.hs
Compiling Relation.Binary in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary.hs
Compiling Relation.Binary.Indexed.Heterogeneous.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Indexed/Heterogeneous/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Core.hs
Compiling Relation.Binary.Indexed.Heterogeneous.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Indexed/Heterogeneous/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Definitions.hs
Compiling Relation.Binary.Indexed.Heterogeneous.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Indexed/Heterogeneous/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Structures.hs
Compiling Relation.Binary.Indexed.Heterogeneous.Bundles in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Indexed/Heterogeneous/Bundles.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Bundles.hs
Compiling Relation.Binary.Indexed.Heterogeneous in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Indexed/Heterogeneous.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous.hs
Compiling Algebra.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Core.hs
Compiling Algebra.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Definitions.hs
Compiling Relation.Binary.Reasoning.Base.Partial in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/Base/Partial.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/Base/Partial.hs
Compiling Relation.Binary.Reasoning.Base.Single in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/Base/Single.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/Base/Single.hs
Compiling Relation.Binary.Reasoning.PartialSetoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/PartialSetoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/PartialSetoid.hs
Compiling Relation.Binary.Reasoning.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/Setoid.hs
Compiling Algebra.Consequences.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Consequences/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Consequences/Base.hs
Compiling Algebra.Consequences.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Consequences/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Consequences/Setoid.hs
Compiling Algebra.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Structures.hs
Compiling Algebra.Bundles in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Bundles.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Bundles.hs
Compiling Algebra in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra.hs
Compiling Relation.Binary.PropositionalEquality.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/PropositionalEquality/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/PropositionalEquality/Properties.hs
Compiling Relation.Binary.PropositionalEquality.Algebra in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/PropositionalEquality/Algebra.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/PropositionalEquality/Algebra.hs
Compiling Relation.Binary.Indexed.Heterogeneous.Construct.Trivial in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.hs
Compiling Function.Equality in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Equality.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Equality.hs
Compiling Axiom.UniquenessOfIdentityProofs in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Axiom/UniquenessOfIdentityProofs.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Axiom/UniquenessOfIdentityProofs.hs
Compiling Axiom.Extensionality.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Axiom/Extensionality/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Axiom/Extensionality/Propositional.hs
Compiling Relation.Binary.PropositionalEquality in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/PropositionalEquality.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/PropositionalEquality.hs
Compiling Induction in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Induction.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Induction.hs
Compiling Function.Definitions.Core1 in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Definitions/Core1.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Definitions/Core1.hs
Compiling Function.Definitions.Core2 in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Definitions/Core2.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Definitions/Core2.hs
Compiling Function.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Definitions.hs
Compiling Function.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Structures.hs
Compiling Function.Bundles in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Bundles.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Bundles.hs
Compiling Function.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Core.hs
Compiling Function in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function.hs
Compiling Induction.WellFounded in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Induction/WellFounded.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Induction/WellFounded.hs
Compiling Relation.Binary.Construct.On in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/On.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/On.hs
Compiling Agda.Builtin.Nat in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Nat.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Nat.hs
Compiling Function.Equivalence in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Equivalence.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Equivalence.hs
Compiling Function.Injection in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Injection.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Injection.hs
Compiling Relation.Nullary.Decidable in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary/Decidable.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary/Decidable.hs
Compiling Data.Unit.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Unit/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Unit/Properties.hs
Compiling Data.Unit in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Unit.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Unit.hs
Compiling Category.Functor in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Category/Functor.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Category/Functor.hs
Compiling Category.Applicative.Indexed in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Category/Applicative/Indexed.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Category/Applicative/Indexed.hs
Compiling Category.Monad.Indexed in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Category/Monad/Indexed.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Category/Monad/Indexed.hs
Compiling Category.Monad in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Category/Monad.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Category/Monad.hs
Compiling Relation.Nullary.Negation in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary/Negation.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary/Negation.hs
Compiling Data.Nat.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Nat/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Nat/Base.hs
Compiling Data.Nat.Properties.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Nat/Properties/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Nat/Properties/Core.hs
Compiling Data.Fin.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Fin/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Fin/Base.hs
Compiling Relation.Nullary.Product in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary/Product.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary/Product.hs
Compiling Algebra.Consequences.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Consequences/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Consequences/Propositional.hs
Compiling Relation.Binary.Reasoning.Base.Triple in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/Base/Triple.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/Base/Triple.hs
Compiling Algebra.Properties.Group in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/Group.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/Group.hs
Compiling Relation.Binary.Morphism.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Morphism/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Morphism/Definitions.hs
Compiling Relation.Binary.Morphism.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Morphism/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Morphism/Structures.hs
Compiling Algebra.Morphism.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Morphism/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Morphism/Definitions.hs
Compiling Algebra.Morphism.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Morphism/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Morphism/Structures.hs
Compiling Algebra.Morphism in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Morphism.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Morphism.hs
Compiling Function.Metric.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Core.hs
Compiling Function.Metric.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Definitions.hs
Compiling Function.Metric.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Structures.hs
Compiling Function.Metric.Bundles in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Bundles.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Bundles.hs
Compiling Function.Metric.Nat.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Nat/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Nat/Core.hs
Compiling Function.Metric.Nat.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Nat/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Nat/Definitions.hs
Compiling Function.Metric.Nat.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Nat/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Nat/Structures.hs
Compiling Function.Metric.Nat.Bundles in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Nat/Bundles.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Nat/Bundles.hs
Compiling Function.Metric.Nat in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Nat.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Nat.hs
Compiling Relation.Binary.Properties.Preorder in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Properties/Preorder.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Properties/Preorder.hs
Compiling Relation.Binary.Construct.NonStrictToStrict in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/NonStrictToStrict.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/NonStrictToStrict.hs
Compiling Relation.Binary.Properties.Poset in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Properties/Poset.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Properties/Poset.hs
Compiling Relation.Binary.Lattice in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Lattice.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Lattice.hs
Compiling Relation.Binary.Construct.NaturalOrder.Left in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/NaturalOrder/Left.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/NaturalOrder/Left.hs
Compiling Algebra.Properties.Semilattice in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/Semilattice.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/Semilattice.hs
Compiling Algebra.Properties.Lattice in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/Lattice.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/Lattice.hs
Compiling Algebra.Properties.DistributiveLattice in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/DistributiveLattice.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/DistributiveLattice.hs
Compiling Algebra.Properties.BooleanAlgebra in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/BooleanAlgebra.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/BooleanAlgebra.hs
Compiling Data.Bool.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Bool/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Bool/Properties.hs
Compiling Data.Nat.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Nat/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Nat/Properties.hs
Compiling Agda.Builtin.List in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/List.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/List.hs
Compiling Relation.Nullary.Sum in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary/Sum.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary/Sum.hs
Compiling Relation.Unary.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Unary/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Unary/Properties.hs
Compiling Data.List.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Base.hs
Compiling Category.Applicative in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Category/Applicative.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Category/Applicative.hs
Compiling Data.List.Relation.Unary.Any in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Unary/Any.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Unary/Any.hs
Compiling Data.List.Membership.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Membership/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Membership/Setoid.hs
Compiling Data.List.Membership.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Membership/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Membership/Propositional.hs
Compiling Data.List.Relation.Unary.All in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Unary/All.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Unary/All.hs
Compiling Data.List.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Properties.hs
Compiling Function.LeftInverse in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/LeftInverse.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/LeftInverse.hs
Compiling Function.Surjection in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Surjection.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Surjection.hs
Compiling Function.Bijection in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Bijection.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Bijection.hs
Compiling Function.Inverse in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Inverse.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Inverse.hs
Compiling Data.List.Relation.Unary.AllPairs.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Unary/AllPairs/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Unary/AllPairs/Core.hs
Compiling Relation.Binary.Construct.Intersection in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/Intersection.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/Intersection.hs
Compiling Data.List.Relation.Unary.AllPairs in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Unary/AllPairs.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Unary/AllPairs.hs
Compiling Data.List.Relation.Binary.Pointwise in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Binary/Pointwise.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Binary/Pointwise.hs
Compiling Data.List.Relation.Binary.Lex.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Binary/Lex/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Binary/Lex/Core.hs
Compiling Data.List.Relation.Binary.Lex.Strict in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Binary/Lex/Strict.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Binary/Lex/Strict.hs
Compiling Agda.Builtin.Char in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Char.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Char.hs
Compiling Agda.Builtin.String in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/String.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/String.hs
Compiling Agda.Builtin.String.Properties in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/String/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/String/Properties.hs
Compiling Data.List.Membership.DecSetoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Membership/DecSetoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Membership/DecSetoid.hs
Compiling Data.List.Membership.DecPropositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Membership/DecPropositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Membership/DecPropositional.hs
Compiling Relation.Binary.Construct.Constant in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/Constant.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/Constant.hs
Compiling Relation.Binary.Construct.Closure.Reflexive in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/Closure/Reflexive.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/Closure/Reflexive.hs
Compiling Data.Char.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Char/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Char/Base.hs
Compiling Data.Vec.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Vec/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Vec/Base.hs
Compiling Data.List.NonEmpty in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/NonEmpty.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/NonEmpty.hs
Compiling Data.List.Relation.Binary.Subset.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Binary/Subset/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Binary/Subset/Setoid.hs
Compiling Data.List.Relation.Binary.Subset.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Binary/Subset/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Binary/Subset/Propositional.hs
Compiling Algebra.Construct.LiftedChoice in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Construct/LiftedChoice.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Construct/LiftedChoice.hs
Compiling Algebra.Construct.NaturalChoice.Min in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Construct/NaturalChoice/Min.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Construct/NaturalChoice/Min.hs
Compiling Relation.Binary.Construct.Converse in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/Converse.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/Converse.hs
Compiling Algebra.Construct.NaturalChoice.Max in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Construct/NaturalChoice/Max.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Construct/NaturalChoice/Max.hs
Compiling Data.List.Extrema.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Extrema/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Extrema/Core.hs
Compiling Function.Related in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Related.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Related.hs
Compiling Data.Product.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Product/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Product/Properties.hs
Compiling Data.Product.Relation.Binary.Pointwise.NonDependent in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Product/Relation/Binary/Pointwise/NonDependent.hs
Compiling Data.Product.Function.NonDependent.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Product/Function/NonDependent/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Product/Function/NonDependent/Setoid.hs
Compiling Function.HalfAdjointEquivalence in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/HalfAdjointEquivalence.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/HalfAdjointEquivalence.hs
Compiling Data.Sum.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Sum/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Sum/Properties.hs
Compiling Relation.Nullary.Indexed in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary/Indexed.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary/Indexed.hs
Compiling Algebra.Structures.Biased in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Structures/Biased.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Structures/Biased.hs
Compiling Data.Unit.Polymorphic.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Unit/Polymorphic/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Unit/Polymorphic/Base.hs
Compiling Data.Unit.Polymorphic.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Unit/Polymorphic/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Unit/Polymorphic/Properties.hs
Compiling Data.Unit.Polymorphic in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Unit/Polymorphic.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Unit/Polymorphic.hs
Compiling Data.Product.Function.NonDependent.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Product/Function/NonDependent/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Product/Function/NonDependent/Propositional.hs
Compiling Data.Empty.Polymorphic in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Empty/Polymorphic.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Empty/Polymorphic.hs
Compiling Data.Sum.Relation.Binary.Pointwise in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Sum/Relation/Binary/Pointwise.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Sum/Relation/Binary/Pointwise.hs
Compiling Data.Sum.Function.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Sum/Function/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Sum/Function/Setoid.hs
Compiling Data.Sum.Function.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Sum/Function/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Sum/Function/Propositional.hs
Compiling Function.Related.TypeIsomorphisms in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Related/TypeIsomorphisms.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Related/TypeIsomorphisms.hs
Compiling Data.Product.Function.Dependent.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Product/Function/Dependent/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Product/Function/Dependent/Propositional.hs
Compiling Data.List.Categorical in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Categorical.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Categorical.hs
Compiling Data.List.Relation.Unary.Unique.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Unary/Unique/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Unary/Unique/Setoid.hs
Compiling Relation.Binary.Properties.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Properties/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Properties/Setoid.hs
Compiling Data.List.Relation.Binary.Equality.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Binary/Equality/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Binary/Equality/Setoid.hs
Compiling Data.Nat in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Nat.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Nat.hs
Compiling Data.Maybe.Relation.Unary.Any in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Maybe/Relation/Unary/Any.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Maybe/Relation/Unary/Any.hs
Compiling Data.List.Membership.Propositional.Properties.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Membership/Propositional/Properties/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Membership/Propositional/Properties/Core.hs
Compiling Data.List.Relation.Unary.Any.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Unary/Any/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Unary/Any/Properties.hs
Compiling Data.List.Membership.Setoid.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Membership/Setoid/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Membership/Setoid/Properties.hs
Compiling Relation.Binary.Properties.TotalOrder in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Properties/TotalOrder.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Properties/TotalOrder.hs
Compiling Relation.Binary.Properties.DecTotalOrder in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Properties/DecTotalOrder.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Properties/DecTotalOrder.hs
Compiling Data.List.Relation.Binary.Equality.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Binary/Equality/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Binary/Equality/Propositional.hs
Compiling Data.List.Membership.Propositional.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Membership/Propositional/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Membership/Propositional/Properties.hs
Compiling Data.List.Extrema in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Extrema.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Extrema.hs
Compiling Relation.Binary.Construct.Subst.Equality in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/Subst/Equality.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/Subst/Equality.hs
Compiling Relation.Binary.Construct.Closure.Reflexive.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/Closure/Reflexive/Properties.hs
Compiling Agda.Builtin.Char.Properties in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Char/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Char/Properties.hs
Compiling Data.Char.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Char/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Char/Properties.hs
Compiling Data.String.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/String/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/String/Base.hs
Compiling Data.String.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/String/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/String/Properties.hs
Compiling Data.Char in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Char.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Char.hs
Compiling Data.String in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/String.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/String.hs
Compiling Agda.Builtin.Size in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Size.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Size.hs
Compiling Size in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Size.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Size.hs
Compiling Data.Maybe.Relation.Unary.All in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Maybe/Relation/Unary/All.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Maybe/Relation/Unary/All.hs
Compiling Data.List.Relation.Unary.All.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Unary/All/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Unary/All/Properties.hs
Compiling Data.Vec.Bounded.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Vec/Bounded/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Vec/Bounded/Base.hs
Compiling Data.Vec in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Vec.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Vec.hs
Compiling Data.Vec.Bounded in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Vec/Bounded.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Vec/Bounded.hs
Compiling Codata.Thunk in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Thunk.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Thunk.hs
Compiling Codata.Conat in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Conat.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Conat.hs
Compiling Codata.Delay in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Delay.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Delay.hs
Compiling Codata.Stream in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Stream.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Stream.hs
Compiling Data.BoundedVec.Inefficient in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/BoundedVec/Inefficient.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/BoundedVec/Inefficient.hs
Compiling Algebra.Properties.AbelianGroup in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/AbelianGroup.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/AbelianGroup.hs
Compiling Algebra.Properties.Ring in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/Ring.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/Ring.hs
Compiling Algebra.Solver.Ring.AlmostCommutativeRing in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Solver/Ring/AlmostCommutativeRing.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Solver/Ring/AlmostCommutativeRing.hs
Compiling Algebra.Definitions.RawMagma in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Definitions/RawMagma.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Definitions/RawMagma.hs
Compiling Data.Vec.Functional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Vec/Functional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Vec/Functional.hs
Compiling Algebra.Definitions.RawMonoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Definitions/RawMonoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Definitions/RawMonoid.hs
Compiling Algebra.Properties.Monoid.Mult in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/Monoid/Mult.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/Monoid/Mult.hs
Compiling Algebra.Definitions.RawSemiring in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Definitions/RawSemiring.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Definitions/RawSemiring.hs
Compiling Algebra.Properties.Semiring.Exp in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/Semiring/Exp.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/Semiring/Exp.hs
Compiling Data.Vec.N-ary in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Vec/N-ary.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Vec/NZ45Zary.hs
Compiling Relation.Binary.Reflection in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reflection.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reflection.hs
Compiling Algebra.Solver.Ring.Lemmas in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Solver/Ring/Lemmas.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Solver/Ring/Lemmas.hs
Compiling Algebra.Solver.Ring in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Solver/Ring.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Solver/Ring.hs
Compiling Algebra.Solver.Ring.Simple in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Solver/Ring/Simple.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Solver/Ring/Simple.hs
Compiling Data.Nat.Solver in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Nat/Solver.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Nat/Solver.hs
Compiling Data.BoundedVec in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/BoundedVec.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/BoundedVec.hs
Compiling Codata.Cowriter in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Cowriter.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Cowriter.hs
Compiling Codata.Colist in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Colist.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Colist.hs
Compiling Relation.Binary.Construct.FromRel in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/FromRel.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/FromRel.hs
Compiling Agda.Builtin.Coinduction in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Coinduction.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Coinduction.hs
Compiling Codata.Musical.Notation in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Musical/Notation.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Musical/Notation.hs
Compiling Codata.Musical.Conat in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Musical/Conat.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Musical/Conat.hs
Compiling Data.Maybe in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Maybe.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Maybe.hs
Compiling Relation.Binary.Reasoning.PartialOrder in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/PartialOrder.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/PartialOrder.hs
Compiling Relation.Binary.Reasoning.Base.Double in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/Base/Double.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/Base/Double.hs
Compiling Relation.Binary.Reasoning.Preorder in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/Preorder.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/Preorder.hs
Compiling Codata.Musical.Colist in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Musical/Colist.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Musical/Colist.hs
Compiling Codata.Musical.Costring in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Musical/Costring.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Musical/Costring.hs
Compiling Agda.Builtin.IO in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/IO.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/IO.hs
Compiling IO.Primitive in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/IO/Primitive.agdai to /Users/satnam/agda-examples/MAlonzo/Code/IO/Primitive.hs
Compiling IO in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/IO.agdai to /Users/satnam/agda-examples/MAlonzo/Code/IO.hs
Compiling hello-world in /Users/satnam/agda-examples/hello-world.agdai to /Users/satnam/agda-examples/MAlonzo/Code/QhelloZ45Zworld.hs
Calling: ghc -O -o /Users/satnam/agda-examples/hello-world -Werror -i/Users/satnam/agda-examples -main-is MAlonzo.Code.QhelloZ45Zworld /Users/satnam/agda-examples/MAlonzo/Code/QhelloZ45Zworld.hs --make -fwarn-incomplete-patterns -fno-warn-overlapping-patterns
[  1 of 130] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
[  2 of 130] Compiling MAlonzo.Code.Agda.Primitive ( MAlonzo/Code/Agda/Primitive.hs, MAlonzo/Code/Agda/Primitive.o )
[  3 of 130] Compiling MAlonzo.Code.Level ( MAlonzo/Code/Level.hs, MAlonzo/Code/Level.o )
[  4 of 130] Compiling MAlonzo.Code.Data.Empty.Polymorphic ( MAlonzo/Code/Data/Empty/Polymorphic.hs, MAlonzo/Code/Data/Empty/Polymorphic.o )
[  5 of 130] Compiling MAlonzo.Code.Data.Empty ( MAlonzo/Code/Data/Empty.hs, MAlonzo/Code/Data/Empty.o )
[  6 of 130] Compiling MAlonzo.Code.Relation.Binary.Definitions ( MAlonzo/Code/Relation/Binary/Definitions.hs, MAlonzo/Code/Relation/Binary/Definitions.o )
[  7 of 130] Compiling MAlonzo.Code.Data.Empty.Irrelevant ( MAlonzo/Code/Data/Empty/Irrelevant.hs, MAlonzo/Code/Data/Empty/Irrelevant.o )
[  8 of 130] Compiling MAlonzo.Code.Relation.Nullary ( MAlonzo/Code/Relation/Nullary.hs, MAlonzo/Code/Relation/Nullary.o )
[  9 of 130] Compiling MAlonzo.Code.Agda.Builtin.Unit ( MAlonzo/Code/Agda/Builtin/Unit.hs, MAlonzo/Code/Agda/Builtin/Unit.o )
[ 10 of 130] Compiling MAlonzo.Code.Agda.Builtin.String ( MAlonzo/Code/Agda/Builtin/String.hs, MAlonzo/Code/Agda/Builtin/String.o )
[ 11 of 130] Compiling MAlonzo.Code.Agda.Builtin.Size ( MAlonzo/Code/Agda/Builtin/Size.hs, MAlonzo/Code/Agda/Builtin/Size.o )
[ 12 of 130] Compiling MAlonzo.Code.Codata.Thunk ( MAlonzo/Code/Codata/Thunk.hs, MAlonzo/Code/Codata/Thunk.o )
[ 13 of 130] Compiling MAlonzo.Code.Codata.Conat ( MAlonzo/Code/Codata/Conat.hs, MAlonzo/Code/Codata/Conat.o )
[ 14 of 130] Compiling MAlonzo.Code.Agda.Builtin.Sigma ( MAlonzo/Code/Agda/Builtin/Sigma.hs, MAlonzo/Code/Agda/Builtin/Sigma.o )
[ 15 of 130] Compiling MAlonzo.Code.Data.Product ( MAlonzo/Code/Data/Product.hs, MAlonzo/Code/Data/Product.o )
[ 16 of 130] Compiling MAlonzo.Code.Agda.Builtin.Nat ( MAlonzo/Code/Agda/Builtin/Nat.hs, MAlonzo/Code/Agda/Builtin/Nat.o )
[ 17 of 130] Compiling MAlonzo.Code.Agda.Builtin.List ( MAlonzo/Code/Agda/Builtin/List.hs, MAlonzo/Code/Agda/Builtin/List.o )
[ 18 of 130] Compiling MAlonzo.Code.Data.BoundedVec.Inefficient ( MAlonzo/Code/Data/BoundedVec/Inefficient.hs, MAlonzo/Code/Data/BoundedVec/Inefficient.o )
[ 19 of 130] Compiling MAlonzo.Code.Agda.Builtin.IO ( MAlonzo/Code/Agda/Builtin/IO.hs, MAlonzo/Code/Agda/Builtin/IO.o )
[ 20 of 130] Compiling MAlonzo.Code.Agda.Builtin.Equality ( MAlonzo/Code/Agda/Builtin/Equality.hs, MAlonzo/Code/Agda/Builtin/Equality.o )
[ 21 of 130] Compiling MAlonzo.Code.Relation.Nullary.Reflects ( MAlonzo/Code/Relation/Nullary/Reflects.hs, MAlonzo/Code/Relation/Nullary/Reflects.o )
[ 22 of 130] Compiling MAlonzo.Code.Relation.Binary.Reasoning.Base.Partial ( MAlonzo/Code/Relation/Binary/Reasoning/Base/Partial.hs, MAlonzo/Code/Relation/Binary/Reasoning/Base/Partial.o )
[ 23 of 130] Compiling MAlonzo.Code.Relation.Binary.PropositionalEquality.Core ( MAlonzo/Code/Relation/Binary/PropositionalEquality/Core.hs, MAlonzo/Code/Relation/Binary/PropositionalEquality/Core.o )
[ 24 of 130] Compiling MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures ( MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Structures.hs, MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Structures.o )
[ 25 of 130] Compiling MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles ( MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Bundles.hs, MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Bundles.o )
[ 26 of 130] Compiling MAlonzo.Code.Category.Functor ( MAlonzo/Code/Category/Functor.hs, MAlonzo/Code/Category/Functor.o )
[ 27 of 130] Compiling MAlonzo.Code.Category.Applicative.Indexed ( MAlonzo/Code/Category/Applicative/Indexed.hs, MAlonzo/Code/Category/Applicative/Indexed.o )
[ 28 of 130] Compiling MAlonzo.Code.Category.Monad.Indexed ( MAlonzo/Code/Category/Monad/Indexed.hs, MAlonzo/Code/Category/Monad/Indexed.o )
[ 29 of 130] Compiling MAlonzo.Code.Agda.Builtin.Coinduction ( MAlonzo/Code/Agda/Builtin/Coinduction.hs, MAlonzo/Code/Agda/Builtin/Coinduction.o )
[ 30 of 130] Compiling MAlonzo.Code.Agda.Builtin.Char ( MAlonzo/Code/Agda/Builtin/Char.hs, MAlonzo/Code/Agda/Builtin/Char.o )
[ 31 of 130] Compiling MAlonzo.Code.Agda.Builtin.Bool ( MAlonzo/Code/Agda/Builtin/Bool.hs, MAlonzo/Code/Agda/Builtin/Bool.o )
[ 32 of 130] Compiling MAlonzo.Code.Data.Sum.Base ( MAlonzo/Code/Data/Sum/Base.hs, MAlonzo/Code/Data/Sum/Base.o )
[ 33 of 130] Compiling MAlonzo.Code.Data.These.Base ( MAlonzo/Code/Data/These/Base.hs, MAlonzo/Code/Data/These/Base.o )
[ 34 of 130] Compiling MAlonzo.Code.Algebra.Consequences.Base ( MAlonzo/Code/Algebra/Consequences/Base.hs, MAlonzo/Code/Algebra/Consequences/Base.o )
[ 35 of 130] Compiling MAlonzo.Code.Data.Nat.Base ( MAlonzo/Code/Data/Nat/Base.hs, MAlonzo/Code/Data/Nat/Base.o )
[ 36 of 130] Compiling MAlonzo.Code.Data.Fin.Base ( MAlonzo/Code/Data/Fin/Base.hs, MAlonzo/Code/Data/Fin/Base.o )
[ 37 of 130] Compiling MAlonzo.Code.Data.Vec.Base ( MAlonzo/Code/Data/Vec/Base.hs, MAlonzo/Code/Data/Vec/Base.o )
[ 38 of 130] Compiling MAlonzo.Code.Data.Bool.Base ( MAlonzo/Code/Data/Bool/Base.hs, MAlonzo/Code/Data/Bool/Base.o )
[ 39 of 130] Compiling MAlonzo.Code.Relation.Nullary.Sum ( MAlonzo/Code/Relation/Nullary/Sum.hs, MAlonzo/Code/Relation/Nullary/Sum.o )
[ 40 of 130] Compiling MAlonzo.Code.Relation.Nullary.Product ( MAlonzo/Code/Relation/Nullary/Product.hs, MAlonzo/Code/Relation/Nullary/Product.o )
[ 41 of 130] Compiling MAlonzo.Code.Relation.Nullary.Decidable.Core ( MAlonzo/Code/Relation/Nullary/Decidable/Core.hs, MAlonzo/Code/Relation/Nullary/Decidable/Core.o )
[ 42 of 130] Compiling MAlonzo.Code.Relation.Nullary.Negation ( MAlonzo/Code/Relation/Nullary/Negation.hs, MAlonzo/Code/Relation/Nullary/Negation.o )
[ 43 of 130] Compiling MAlonzo.Code.Relation.Unary.Properties ( MAlonzo/Code/Relation/Unary/Properties.hs, MAlonzo/Code/Relation/Unary/Properties.o )
[ 44 of 130] Compiling MAlonzo.Code.Data.Maybe.Base ( MAlonzo/Code/Data/Maybe/Base.hs, MAlonzo/Code/Data/Maybe/Base.o )
[ 45 of 130] Compiling MAlonzo.Code.Relation.Binary.Consequences ( MAlonzo/Code/Relation/Binary/Consequences.hs, MAlonzo/Code/Relation/Binary/Consequences.o )
[ 46 of 130] Compiling MAlonzo.Code.Relation.Binary.Structures ( MAlonzo/Code/Relation/Binary/Structures.hs, MAlonzo/Code/Relation/Binary/Structures.o )
[ 47 of 130] Compiling MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple ( MAlonzo/Code/Relation/Binary/Reasoning/Base/Triple.hs, MAlonzo/Code/Relation/Binary/Reasoning/Base/Triple.o )
[ 48 of 130] Compiling MAlonzo.Code.Relation.Binary.Reasoning.Base.Double ( MAlonzo/Code/Relation/Binary/Reasoning/Base/Double.hs, MAlonzo/Code/Relation/Binary/Reasoning/Base/Double.o )
[ 49 of 130] Compiling MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict ( MAlonzo/Code/Relation/Binary/Construct/NonStrictToStrict.hs, MAlonzo/Code/Relation/Binary/Construct/NonStrictToStrict.o )
[ 50 of 130] Compiling MAlonzo.Code.Function.Metric.Structures ( MAlonzo/Code/Function/Metric/Structures.hs, MAlonzo/Code/Function/Metric/Structures.o )
[ 51 of 130] Compiling MAlonzo.Code.Function.Metric.Nat.Bundles ( MAlonzo/Code/Function/Metric/Nat/Bundles.hs, MAlonzo/Code/Function/Metric/Nat/Bundles.o )
[ 52 of 130] Compiling MAlonzo.Code.Relation.Binary.Bundles ( MAlonzo/Code/Relation/Binary/Bundles.hs, MAlonzo/Code/Relation/Binary/Bundles.o )
[ 53 of 130] Compiling MAlonzo.Code.Relation.Binary.Reasoning.PartialSetoid ( MAlonzo/Code/Relation/Binary/Reasoning/PartialSetoid.hs, MAlonzo/Code/Relation/Binary/Reasoning/PartialSetoid.o )
[ 54 of 130] Compiling MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties ( MAlonzo/Code/Relation/Binary/PropositionalEquality/Properties.hs, MAlonzo/Code/Relation/Binary/PropositionalEquality/Properties.o )
[ 55 of 130] Compiling MAlonzo.Code.Relation.Binary.Properties.Preorder ( MAlonzo/Code/Relation/Binary/Properties/Preorder.hs, MAlonzo/Code/Relation/Binary/Properties/Preorder.o )
[ 56 of 130] Compiling MAlonzo.Code.Relation.Binary.Properties.Poset ( MAlonzo/Code/Relation/Binary/Properties/Poset.hs, MAlonzo/Code/Relation/Binary/Properties/Poset.o )
[ 57 of 130] Compiling MAlonzo.Code.Relation.Binary.Lattice ( MAlonzo/Code/Relation/Binary/Lattice.hs, MAlonzo/Code/Relation/Binary/Lattice.o )
[ 58 of 130] Compiling MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Construct.Trivial ( MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.hs, MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.o )
[ 59 of 130] Compiling MAlonzo.Code.Relation.Binary.Construct.FromRel ( MAlonzo/Code/Relation/Binary/Construct/FromRel.hs, MAlonzo/Code/Relation/Binary/Construct/FromRel.o )
[ 60 of 130] Compiling MAlonzo.Code.Relation.Binary.Construct.Converse ( MAlonzo/Code/Relation/Binary/Construct/Converse.hs, MAlonzo/Code/Relation/Binary/Construct/Converse.o )
[ 61 of 130] Compiling MAlonzo.Code.Function.Structures ( MAlonzo/Code/Function/Structures.hs, MAlonzo/Code/Function/Structures.o )
[ 62 of 130] Compiling MAlonzo.Code.Function.Equality ( MAlonzo/Code/Function/Equality.hs, MAlonzo/Code/Function/Equality.o )
[ 63 of 130] Compiling MAlonzo.Code.Relation.Binary.PropositionalEquality ( MAlonzo/Code/Relation/Binary/PropositionalEquality.hs, MAlonzo/Code/Relation/Binary/PropositionalEquality.o )
[ 64 of 130] Compiling MAlonzo.Code.Function.Injection ( MAlonzo/Code/Function/Injection.hs, MAlonzo/Code/Function/Injection.o )
[ 65 of 130] Compiling MAlonzo.Code.Function.Equivalence ( MAlonzo/Code/Function/Equivalence.hs, MAlonzo/Code/Function/Equivalence.o )
[ 66 of 130] Compiling MAlonzo.Code.Function.LeftInverse ( MAlonzo/Code/Function/LeftInverse.hs, MAlonzo/Code/Function/LeftInverse.o )
[ 67 of 130] Compiling MAlonzo.Code.Function.Surjection ( MAlonzo/Code/Function/Surjection.hs, MAlonzo/Code/Function/Surjection.o )
[ 68 of 130] Compiling MAlonzo.Code.Function.Bundles ( MAlonzo/Code/Function/Bundles.hs, MAlonzo/Code/Function/Bundles.o )
[ 69 of 130] Compiling MAlonzo.Code.Relation.Nullary.Decidable ( MAlonzo/Code/Relation/Nullary/Decidable.hs, MAlonzo/Code/Relation/Nullary/Decidable.o )
[ 70 of 130] Compiling MAlonzo.Code.Data.Product.Properties ( MAlonzo/Code/Data/Product/Properties.hs, MAlonzo/Code/Data/Product/Properties.o )
[ 71 of 130] Compiling MAlonzo.Code.Function.Bijection ( MAlonzo/Code/Function/Bijection.hs, MAlonzo/Code/Function/Bijection.o )
[ 72 of 130] Compiling MAlonzo.Code.Function.Inverse ( MAlonzo/Code/Function/Inverse.hs, MAlonzo/Code/Function/Inverse.o )
[ 73 of 130] Compiling MAlonzo.Code.Function.Related ( MAlonzo/Code/Function/Related.hs, MAlonzo/Code/Function/Related.o )
[ 74 of 130] Compiling MAlonzo.Code.Function.HalfAdjointEquivalence ( MAlonzo/Code/Function/HalfAdjointEquivalence.hs, MAlonzo/Code/Function/HalfAdjointEquivalence.o )
[ 75 of 130] Compiling MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise ( MAlonzo/Code/Data/Sum/Relation/Binary/Pointwise.hs, MAlonzo/Code/Data/Sum/Relation/Binary/Pointwise.o )
[ 76 of 130] Compiling MAlonzo.Code.Data.Sum.Function.Setoid ( MAlonzo/Code/Data/Sum/Function/Setoid.hs, MAlonzo/Code/Data/Sum/Function/Setoid.o )
[ 77 of 130] Compiling MAlonzo.Code.Data.Sum.Function.Propositional ( MAlonzo/Code/Data/Sum/Function/Propositional.hs, MAlonzo/Code/Data/Sum/Function/Propositional.o )
[ 78 of 130] Compiling MAlonzo.Code.Data.Product.Relation.Binary.Pointwise.NonDependent ( MAlonzo/Code/Data/Product/Relation/Binary/Pointwise/NonDependent.hs, MAlonzo/Code/Data/Product/Relation/Binary/Pointwise/NonDependent.o )
[ 79 of 130] Compiling MAlonzo.Code.Data.Product.Function.NonDependent.Setoid ( MAlonzo/Code/Data/Product/Function/NonDependent/Setoid.hs, MAlonzo/Code/Data/Product/Function/NonDependent/Setoid.o )
[ 80 of 130] Compiling MAlonzo.Code.Data.Product.Function.NonDependent.Propositional ( MAlonzo/Code/Data/Product/Function/NonDependent/Propositional.hs, MAlonzo/Code/Data/Product/Function/NonDependent/Propositional.o )
[ 81 of 130] Compiling MAlonzo.Code.Data.Product.Function.Dependent.Propositional ( MAlonzo/Code/Data/Product/Function/Dependent/Propositional.hs, MAlonzo/Code/Data/Product/Function/Dependent/Propositional.o )
[ 82 of 130] Compiling MAlonzo.Code.Codata.Musical.Conat ( MAlonzo/Code/Codata/Musical/Conat.hs, MAlonzo/Code/Codata/Musical/Conat.o )
[ 83 of 130] Compiling MAlonzo.Code.Algebra.Consequences.Setoid ( MAlonzo/Code/Algebra/Consequences/Setoid.hs, MAlonzo/Code/Algebra/Consequences/Setoid.o )
[ 84 of 130] Compiling MAlonzo.Code.Algebra.Structures ( MAlonzo/Code/Algebra/Structures.hs, MAlonzo/Code/Algebra/Structures.o )
[ 85 of 130] Compiling MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left ( MAlonzo/Code/Relation/Binary/Construct/NaturalOrder/Left.hs, MAlonzo/Code/Relation/Binary/Construct/NaturalOrder/Left.o )
[ 86 of 130] Compiling MAlonzo.Code.Algebra.Structures.Biased ( MAlonzo/Code/Algebra/Structures/Biased.hs, MAlonzo/Code/Algebra/Structures/Biased.o )
[ 87 of 130] Compiling MAlonzo.Code.Algebra.Construct.LiftedChoice ( MAlonzo/Code/Algebra/Construct/LiftedChoice.hs, MAlonzo/Code/Algebra/Construct/LiftedChoice.o )
[ 88 of 130] Compiling MAlonzo.Code.Algebra.Bundles ( MAlonzo/Code/Algebra/Bundles.hs, MAlonzo/Code/Algebra/Bundles.o )
[ 89 of 130] Compiling MAlonzo.Code.Relation.Binary.PropositionalEquality.Algebra ( MAlonzo/Code/Relation/Binary/PropositionalEquality/Algebra.hs, MAlonzo/Code/Relation/Binary/PropositionalEquality/Algebra.o )
[ 90 of 130] Compiling MAlonzo.Code.Function.Related.TypeIsomorphisms ( MAlonzo/Code/Function/Related/TypeIsomorphisms.hs, MAlonzo/Code/Function/Related/TypeIsomorphisms.o )
[ 91 of 130] Compiling MAlonzo.Code.Algebra.Properties.Semilattice ( MAlonzo/Code/Algebra/Properties/Semilattice.hs, MAlonzo/Code/Algebra/Properties/Semilattice.o )
[ 92 of 130] Compiling MAlonzo.Code.Algebra.Properties.Lattice ( MAlonzo/Code/Algebra/Properties/Lattice.hs, MAlonzo/Code/Algebra/Properties/Lattice.o )
[ 93 of 130] Compiling MAlonzo.Code.Algebra.Properties.DistributiveLattice ( MAlonzo/Code/Algebra/Properties/DistributiveLattice.hs, MAlonzo/Code/Algebra/Properties/DistributiveLattice.o )
[ 94 of 130] Compiling MAlonzo.Code.Algebra.Morphism ( MAlonzo/Code/Algebra/Morphism.hs, MAlonzo/Code/Algebra/Morphism.o )
[ 95 of 130] Compiling MAlonzo.Code.Algebra.Construct.NaturalChoice.Min ( MAlonzo/Code/Algebra/Construct/NaturalChoice/Min.hs, MAlonzo/Code/Algebra/Construct/NaturalChoice/Min.o )
[ 96 of 130] Compiling MAlonzo.Code.Data.List.Extrema.Core ( MAlonzo/Code/Data/List/Extrema/Core.hs, MAlonzo/Code/Data/List/Extrema/Core.o )
[ 97 of 130] Compiling MAlonzo.Code.Algebra.Properties.BooleanAlgebra ( MAlonzo/Code/Algebra/Properties/BooleanAlgebra.hs, MAlonzo/Code/Algebra/Properties/BooleanAlgebra.o )
[ 98 of 130] Compiling MAlonzo.Code.Data.Maybe.Relation.Unary.Any ( MAlonzo/Code/Data/Maybe/Relation/Unary/Any.hs, MAlonzo/Code/Data/Maybe/Relation/Unary/Any.o )
[ 99 of 130] Compiling MAlonzo.Code.Data.Maybe.Relation.Unary.All ( MAlonzo/Code/Data/Maybe/Relation/Unary/All.hs, MAlonzo/Code/Data/Maybe/Relation/Unary/All.o )
[100 of 130] Compiling MAlonzo.Code.Codata.Delay ( MAlonzo/Code/Codata/Delay.hs, MAlonzo/Code/Codata/Delay.o )
[101 of 130] Compiling MAlonzo.Code.Data.List.Base ( MAlonzo/Code/Data/List/Base.hs, MAlonzo/Code/Data/List/Base.o )
[102 of 130] Compiling MAlonzo.Code.Data.List.Relation.Unary.Any ( MAlonzo/Code/Data/List/Relation/Unary/Any.hs, MAlonzo/Code/Data/List/Relation/Unary/Any.o )
[103 of 130] Compiling MAlonzo.Code.Data.List.Relation.Unary.All ( MAlonzo/Code/Data/List/Relation/Unary/All.hs, MAlonzo/Code/Data/List/Relation/Unary/All.o )
[104 of 130] Compiling MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core ( MAlonzo/Code/Data/List/Relation/Unary/AllPairs/Core.hs, MAlonzo/Code/Data/List/Relation/Unary/AllPairs/Core.o )
[105 of 130] Compiling MAlonzo.Code.Data.List.Membership.Setoid ( MAlonzo/Code/Data/List/Membership/Setoid.hs, MAlonzo/Code/Data/List/Membership/Setoid.o )
[106 of 130] Compiling MAlonzo.Code.Data.List.Membership.Propositional ( MAlonzo/Code/Data/List/Membership/Propositional.hs, MAlonzo/Code/Data/List/Membership/Propositional.o )
[107 of 130] Compiling MAlonzo.Code.Data.List.Membership.Propositional.Properties.Core ( MAlonzo/Code/Data/List/Membership/Propositional/Properties/Core.hs, MAlonzo/Code/Data/List/Membership/Propositional/Properties/Core.o )
[108 of 130] Compiling MAlonzo.Code.Data.List.Categorical ( MAlonzo/Code/Data/List/Categorical.hs, MAlonzo/Code/Data/List/Categorical.o )
[109 of 130] Compiling MAlonzo.Code.Data.BoundedVec ( MAlonzo/Code/Data/BoundedVec.hs, MAlonzo/Code/Data/BoundedVec.o )
[110 of 130] Compiling MAlonzo.Code.Data.Bool.Properties ( MAlonzo/Code/Data/Bool/Properties.hs, MAlonzo/Code/Data/Bool/Properties.o )
[111 of 130] Compiling MAlonzo.Code.Data.Nat.Properties ( MAlonzo/Code/Data/Nat/Properties.hs, MAlonzo/Code/Data/Nat/Properties.o )
[112 of 130] Compiling MAlonzo.Code.Data.List.Properties ( MAlonzo/Code/Data/List/Properties.hs, MAlonzo/Code/Data/List/Properties.o )
[113 of 130] Compiling MAlonzo.Code.Data.List.Relation.Binary.Pointwise ( MAlonzo/Code/Data/List/Relation/Binary/Pointwise.hs, MAlonzo/Code/Data/List/Relation/Binary/Pointwise.o )
[114 of 130] Compiling MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid ( MAlonzo/Code/Data/List/Relation/Binary/Equality/Setoid.hs, MAlonzo/Code/Data/List/Relation/Binary/Equality/Setoid.o )
[115 of 130] Compiling MAlonzo.Code.Data.List.Relation.Binary.Equality.Propositional ( MAlonzo/Code/Data/List/Relation/Binary/Equality/Propositional.hs, MAlonzo/Code/Data/List/Relation/Binary/Equality/Propositional.o )
[116 of 130] Compiling MAlonzo.Code.Data.List.Relation.Unary.Any.Properties ( MAlonzo/Code/Data/List/Relation/Unary/Any/Properties.hs, MAlonzo/Code/Data/List/Relation/Unary/Any/Properties.o )
[117 of 130] Compiling MAlonzo.Code.Data.List.Membership.Setoid.Properties ( MAlonzo/Code/Data/List/Membership/Setoid/Properties.hs, MAlonzo/Code/Data/List/Membership/Setoid/Properties.o )
[118 of 130] Compiling MAlonzo.Code.Data.List.Membership.Propositional.Properties ( MAlonzo/Code/Data/List/Membership/Propositional/Properties.hs, MAlonzo/Code/Data/List/Membership/Propositional/Properties.o )
[119 of 130] Compiling MAlonzo.Code.Data.List.Extrema ( MAlonzo/Code/Data/List/Extrema.hs, MAlonzo/Code/Data/List/Extrema.o )
[120 of 130] Compiling MAlonzo.Code.Data.List.Relation.Unary.All.Properties ( MAlonzo/Code/Data/List/Relation/Unary/All/Properties.hs, MAlonzo/Code/Data/List/Relation/Unary/All/Properties.o )
[121 of 130] Compiling MAlonzo.Code.Data.Vec.Bounded.Base ( MAlonzo/Code/Data/Vec/Bounded/Base.hs, MAlonzo/Code/Data/Vec/Bounded/Base.o )
[122 of 130] Compiling MAlonzo.Code.Data.List.NonEmpty ( MAlonzo/Code/Data/List/NonEmpty.hs, MAlonzo/Code/Data/List/NonEmpty.o )
[123 of 130] Compiling MAlonzo.Code.Codata.Stream ( MAlonzo/Code/Codata/Stream.hs, MAlonzo/Code/Codata/Stream.o )
[124 of 130] Compiling MAlonzo.Code.Codata.Cowriter ( MAlonzo/Code/Codata/Cowriter.hs, MAlonzo/Code/Codata/Cowriter.o )
[125 of 130] Compiling MAlonzo.Code.Codata.Colist ( MAlonzo/Code/Codata/Colist.hs, MAlonzo/Code/Codata/Colist.o )
[126 of 130] Compiling MAlonzo.Code.Codata.Musical.Colist ( MAlonzo/Code/Codata/Musical/Colist.hs, MAlonzo/Code/Codata/Musical/Colist.o )
[127 of 130] Compiling MAlonzo.Code.IO.Primitive ( MAlonzo/Code/IO/Primitive.hs, MAlonzo/Code/IO/Primitive.o )
[128 of 130] Compiling MAlonzo.Code.Codata.Musical.Costring ( MAlonzo/Code/Codata/Musical/Costring.hs, MAlonzo/Code/Codata/Musical/Costring.o )
[129 of 130] Compiling MAlonzo.Code.IO  ( MAlonzo/Code/IO.hs, MAlonzo/Code/IO.o )
[130 of 130] Compiling MAlonzo.Code.QhelloZ45Zworld ( /Users/satnam/agda-examples/MAlonzo/Code/QhelloZ45Zworld.hs, /Users/satnam/agda-examples/MAlonzo/Code/QhelloZ45Zworld.o )
Linking /Users/satnam/agda-examples/hello-world ...
satnam-macbookpro3:agda-examples satnam$ ./hello-world
Hello, World!

All 3 comments

We've just pushed an update (#5223) because the hello world example in
the user manual was broken by a recent update to the stdlib shipped
as part of 1.5.

The gist of it is:

open import Level
open import IO

main = run {0鈩搣 (putStrLn "Hello, World!")

The development version of the manual has a neater solution but you'll need
to wait for the next release of the stdlib to be able to use it.

Thank you. That works! Now I can start to actually try and learn some Agda!
I was not expecting this to actually build the world :-)

$ agda --compile hello-world.agda
Checking hello-world (/Users/satnam/agda-examples/hello-world.agda).
Compiling Agda.Primitive in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Primitive.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Primitive.hs
Compiling Agda.Builtin.Equality in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Equality.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Equality.hs
Compiling Data.Empty in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Empty.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Empty.hs
Compiling Data.Empty.Irrelevant in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Empty/Irrelevant.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Empty/Irrelevant.hs
Compiling Agda.Builtin.Bool in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Bool.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Bool.hs
Compiling Agda.Builtin.Unit in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Unit.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Unit.hs
Compiling Data.Unit.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Unit/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Unit/Base.hs
Compiling Level in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Level.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Level.hs
Compiling Data.Bool.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Bool/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Bool/Base.hs
Compiling Relation.Nullary in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary.hs
Compiling Relation.Nullary.Reflects in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary/Reflects.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary/Reflects.hs
Compiling Agda.Builtin.Strict in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Strict.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Strict.hs
Compiling Strict in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Strict.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Strict.hs
Compiling Function.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Base.hs
Compiling Data.Sum.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Sum/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Sum/Base.hs
Compiling Data.These.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/These/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/These/Base.hs
Compiling Agda.Builtin.Sigma in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Sigma.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Sigma.hs
Compiling Data.Product in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Product.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Product.hs
Compiling Data.Maybe.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Maybe/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Maybe/Base.hs
Compiling Relation.Binary.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Core.hs
Compiling Relation.Binary.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Definitions.hs
Compiling Relation.Binary.PropositionalEquality.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/PropositionalEquality/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/PropositionalEquality/Core.hs
Compiling Relation.Nullary.Decidable.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary/Decidable/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary/Decidable/Core.hs
Compiling Relation.Unary in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Unary.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Unary.hs
Compiling Relation.Binary.Consequences in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Consequences.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Consequences.hs
Compiling Relation.Binary.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Structures.hs
Compiling Relation.Binary.Bundles in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Bundles.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Bundles.hs
Compiling Relation.Binary in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary.hs
Compiling Relation.Binary.Indexed.Heterogeneous.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Indexed/Heterogeneous/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Core.hs
Compiling Relation.Binary.Indexed.Heterogeneous.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Indexed/Heterogeneous/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Definitions.hs
Compiling Relation.Binary.Indexed.Heterogeneous.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Indexed/Heterogeneous/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Structures.hs
Compiling Relation.Binary.Indexed.Heterogeneous.Bundles in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Indexed/Heterogeneous/Bundles.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Bundles.hs
Compiling Relation.Binary.Indexed.Heterogeneous in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Indexed/Heterogeneous.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous.hs
Compiling Algebra.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Core.hs
Compiling Algebra.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Definitions.hs
Compiling Relation.Binary.Reasoning.Base.Partial in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/Base/Partial.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/Base/Partial.hs
Compiling Relation.Binary.Reasoning.Base.Single in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/Base/Single.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/Base/Single.hs
Compiling Relation.Binary.Reasoning.PartialSetoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/PartialSetoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/PartialSetoid.hs
Compiling Relation.Binary.Reasoning.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/Setoid.hs
Compiling Algebra.Consequences.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Consequences/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Consequences/Base.hs
Compiling Algebra.Consequences.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Consequences/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Consequences/Setoid.hs
Compiling Algebra.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Structures.hs
Compiling Algebra.Bundles in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Bundles.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Bundles.hs
Compiling Algebra in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra.hs
Compiling Relation.Binary.PropositionalEquality.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/PropositionalEquality/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/PropositionalEquality/Properties.hs
Compiling Relation.Binary.PropositionalEquality.Algebra in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/PropositionalEquality/Algebra.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/PropositionalEquality/Algebra.hs
Compiling Relation.Binary.Indexed.Heterogeneous.Construct.Trivial in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.hs
Compiling Function.Equality in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Equality.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Equality.hs
Compiling Axiom.UniquenessOfIdentityProofs in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Axiom/UniquenessOfIdentityProofs.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Axiom/UniquenessOfIdentityProofs.hs
Compiling Axiom.Extensionality.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Axiom/Extensionality/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Axiom/Extensionality/Propositional.hs
Compiling Relation.Binary.PropositionalEquality in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/PropositionalEquality.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/PropositionalEquality.hs
Compiling Induction in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Induction.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Induction.hs
Compiling Function.Definitions.Core1 in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Definitions/Core1.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Definitions/Core1.hs
Compiling Function.Definitions.Core2 in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Definitions/Core2.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Definitions/Core2.hs
Compiling Function.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Definitions.hs
Compiling Function.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Structures.hs
Compiling Function.Bundles in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Bundles.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Bundles.hs
Compiling Function.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Core.hs
Compiling Function in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function.hs
Compiling Induction.WellFounded in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Induction/WellFounded.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Induction/WellFounded.hs
Compiling Relation.Binary.Construct.On in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/On.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/On.hs
Compiling Agda.Builtin.Nat in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Nat.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Nat.hs
Compiling Function.Equivalence in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Equivalence.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Equivalence.hs
Compiling Function.Injection in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Injection.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Injection.hs
Compiling Relation.Nullary.Decidable in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary/Decidable.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary/Decidable.hs
Compiling Data.Unit.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Unit/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Unit/Properties.hs
Compiling Data.Unit in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Unit.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Unit.hs
Compiling Category.Functor in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Category/Functor.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Category/Functor.hs
Compiling Category.Applicative.Indexed in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Category/Applicative/Indexed.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Category/Applicative/Indexed.hs
Compiling Category.Monad.Indexed in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Category/Monad/Indexed.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Category/Monad/Indexed.hs
Compiling Category.Monad in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Category/Monad.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Category/Monad.hs
Compiling Relation.Nullary.Negation in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary/Negation.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary/Negation.hs
Compiling Data.Nat.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Nat/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Nat/Base.hs
Compiling Data.Nat.Properties.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Nat/Properties/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Nat/Properties/Core.hs
Compiling Data.Fin.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Fin/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Fin/Base.hs
Compiling Relation.Nullary.Product in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary/Product.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary/Product.hs
Compiling Algebra.Consequences.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Consequences/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Consequences/Propositional.hs
Compiling Relation.Binary.Reasoning.Base.Triple in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/Base/Triple.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/Base/Triple.hs
Compiling Algebra.Properties.Group in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/Group.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/Group.hs
Compiling Relation.Binary.Morphism.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Morphism/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Morphism/Definitions.hs
Compiling Relation.Binary.Morphism.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Morphism/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Morphism/Structures.hs
Compiling Algebra.Morphism.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Morphism/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Morphism/Definitions.hs
Compiling Algebra.Morphism.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Morphism/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Morphism/Structures.hs
Compiling Algebra.Morphism in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Morphism.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Morphism.hs
Compiling Function.Metric.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Core.hs
Compiling Function.Metric.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Definitions.hs
Compiling Function.Metric.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Structures.hs
Compiling Function.Metric.Bundles in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Bundles.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Bundles.hs
Compiling Function.Metric.Nat.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Nat/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Nat/Core.hs
Compiling Function.Metric.Nat.Definitions in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Nat/Definitions.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Nat/Definitions.hs
Compiling Function.Metric.Nat.Structures in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Nat/Structures.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Nat/Structures.hs
Compiling Function.Metric.Nat.Bundles in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Nat/Bundles.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Nat/Bundles.hs
Compiling Function.Metric.Nat in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Metric/Nat.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Metric/Nat.hs
Compiling Relation.Binary.Properties.Preorder in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Properties/Preorder.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Properties/Preorder.hs
Compiling Relation.Binary.Construct.NonStrictToStrict in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/NonStrictToStrict.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/NonStrictToStrict.hs
Compiling Relation.Binary.Properties.Poset in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Properties/Poset.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Properties/Poset.hs
Compiling Relation.Binary.Lattice in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Lattice.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Lattice.hs
Compiling Relation.Binary.Construct.NaturalOrder.Left in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/NaturalOrder/Left.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/NaturalOrder/Left.hs
Compiling Algebra.Properties.Semilattice in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/Semilattice.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/Semilattice.hs
Compiling Algebra.Properties.Lattice in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/Lattice.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/Lattice.hs
Compiling Algebra.Properties.DistributiveLattice in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/DistributiveLattice.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/DistributiveLattice.hs
Compiling Algebra.Properties.BooleanAlgebra in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/BooleanAlgebra.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/BooleanAlgebra.hs
Compiling Data.Bool.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Bool/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Bool/Properties.hs
Compiling Data.Nat.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Nat/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Nat/Properties.hs
Compiling Agda.Builtin.List in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/List.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/List.hs
Compiling Relation.Nullary.Sum in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary/Sum.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary/Sum.hs
Compiling Relation.Unary.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Unary/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Unary/Properties.hs
Compiling Data.List.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Base.hs
Compiling Category.Applicative in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Category/Applicative.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Category/Applicative.hs
Compiling Data.List.Relation.Unary.Any in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Unary/Any.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Unary/Any.hs
Compiling Data.List.Membership.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Membership/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Membership/Setoid.hs
Compiling Data.List.Membership.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Membership/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Membership/Propositional.hs
Compiling Data.List.Relation.Unary.All in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Unary/All.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Unary/All.hs
Compiling Data.List.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Properties.hs
Compiling Function.LeftInverse in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/LeftInverse.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/LeftInverse.hs
Compiling Function.Surjection in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Surjection.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Surjection.hs
Compiling Function.Bijection in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Bijection.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Bijection.hs
Compiling Function.Inverse in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Inverse.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Inverse.hs
Compiling Data.List.Relation.Unary.AllPairs.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Unary/AllPairs/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Unary/AllPairs/Core.hs
Compiling Relation.Binary.Construct.Intersection in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/Intersection.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/Intersection.hs
Compiling Data.List.Relation.Unary.AllPairs in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Unary/AllPairs.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Unary/AllPairs.hs
Compiling Data.List.Relation.Binary.Pointwise in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Binary/Pointwise.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Binary/Pointwise.hs
Compiling Data.List.Relation.Binary.Lex.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Binary/Lex/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Binary/Lex/Core.hs
Compiling Data.List.Relation.Binary.Lex.Strict in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Binary/Lex/Strict.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Binary/Lex/Strict.hs
Compiling Agda.Builtin.Char in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Char.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Char.hs
Compiling Agda.Builtin.String in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/String.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/String.hs
Compiling Agda.Builtin.String.Properties in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/String/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/String/Properties.hs
Compiling Data.List.Membership.DecSetoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Membership/DecSetoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Membership/DecSetoid.hs
Compiling Data.List.Membership.DecPropositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Membership/DecPropositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Membership/DecPropositional.hs
Compiling Relation.Binary.Construct.Constant in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/Constant.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/Constant.hs
Compiling Relation.Binary.Construct.Closure.Reflexive in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/Closure/Reflexive.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/Closure/Reflexive.hs
Compiling Data.Char.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Char/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Char/Base.hs
Compiling Data.Vec.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Vec/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Vec/Base.hs
Compiling Data.List.NonEmpty in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/NonEmpty.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/NonEmpty.hs
Compiling Data.List.Relation.Binary.Subset.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Binary/Subset/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Binary/Subset/Setoid.hs
Compiling Data.List.Relation.Binary.Subset.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Binary/Subset/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Binary/Subset/Propositional.hs
Compiling Algebra.Construct.LiftedChoice in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Construct/LiftedChoice.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Construct/LiftedChoice.hs
Compiling Algebra.Construct.NaturalChoice.Min in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Construct/NaturalChoice/Min.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Construct/NaturalChoice/Min.hs
Compiling Relation.Binary.Construct.Converse in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/Converse.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/Converse.hs
Compiling Algebra.Construct.NaturalChoice.Max in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Construct/NaturalChoice/Max.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Construct/NaturalChoice/Max.hs
Compiling Data.List.Extrema.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Extrema/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Extrema/Core.hs
Compiling Function.Related in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Related.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Related.hs
Compiling Data.Product.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Product/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Product/Properties.hs
Compiling Data.Product.Relation.Binary.Pointwise.NonDependent in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Product/Relation/Binary/Pointwise/NonDependent.hs
Compiling Data.Product.Function.NonDependent.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Product/Function/NonDependent/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Product/Function/NonDependent/Setoid.hs
Compiling Function.HalfAdjointEquivalence in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/HalfAdjointEquivalence.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/HalfAdjointEquivalence.hs
Compiling Data.Sum.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Sum/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Sum/Properties.hs
Compiling Relation.Nullary.Indexed in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Nullary/Indexed.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Nullary/Indexed.hs
Compiling Algebra.Structures.Biased in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Structures/Biased.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Structures/Biased.hs
Compiling Data.Unit.Polymorphic.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Unit/Polymorphic/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Unit/Polymorphic/Base.hs
Compiling Data.Unit.Polymorphic.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Unit/Polymorphic/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Unit/Polymorphic/Properties.hs
Compiling Data.Unit.Polymorphic in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Unit/Polymorphic.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Unit/Polymorphic.hs
Compiling Data.Product.Function.NonDependent.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Product/Function/NonDependent/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Product/Function/NonDependent/Propositional.hs
Compiling Data.Empty.Polymorphic in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Empty/Polymorphic.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Empty/Polymorphic.hs
Compiling Data.Sum.Relation.Binary.Pointwise in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Sum/Relation/Binary/Pointwise.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Sum/Relation/Binary/Pointwise.hs
Compiling Data.Sum.Function.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Sum/Function/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Sum/Function/Setoid.hs
Compiling Data.Sum.Function.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Sum/Function/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Sum/Function/Propositional.hs
Compiling Function.Related.TypeIsomorphisms in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Function/Related/TypeIsomorphisms.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Function/Related/TypeIsomorphisms.hs
Compiling Data.Product.Function.Dependent.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Product/Function/Dependent/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Product/Function/Dependent/Propositional.hs
Compiling Data.List.Categorical in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Categorical.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Categorical.hs
Compiling Data.List.Relation.Unary.Unique.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Unary/Unique/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Unary/Unique/Setoid.hs
Compiling Relation.Binary.Properties.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Properties/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Properties/Setoid.hs
Compiling Data.List.Relation.Binary.Equality.Setoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Binary/Equality/Setoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Binary/Equality/Setoid.hs
Compiling Data.Nat in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Nat.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Nat.hs
Compiling Data.Maybe.Relation.Unary.Any in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Maybe/Relation/Unary/Any.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Maybe/Relation/Unary/Any.hs
Compiling Data.List.Membership.Propositional.Properties.Core in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Membership/Propositional/Properties/Core.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Membership/Propositional/Properties/Core.hs
Compiling Data.List.Relation.Unary.Any.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Unary/Any/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Unary/Any/Properties.hs
Compiling Data.List.Membership.Setoid.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Membership/Setoid/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Membership/Setoid/Properties.hs
Compiling Relation.Binary.Properties.TotalOrder in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Properties/TotalOrder.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Properties/TotalOrder.hs
Compiling Relation.Binary.Properties.DecTotalOrder in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Properties/DecTotalOrder.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Properties/DecTotalOrder.hs
Compiling Data.List.Relation.Binary.Equality.Propositional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Binary/Equality/Propositional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Binary/Equality/Propositional.hs
Compiling Data.List.Membership.Propositional.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Membership/Propositional/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Membership/Propositional/Properties.hs
Compiling Data.List.Extrema in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Extrema.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Extrema.hs
Compiling Relation.Binary.Construct.Subst.Equality in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/Subst/Equality.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/Subst/Equality.hs
Compiling Relation.Binary.Construct.Closure.Reflexive.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/Closure/Reflexive/Properties.hs
Compiling Agda.Builtin.Char.Properties in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Char/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Char/Properties.hs
Compiling Data.Char.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Char/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Char/Properties.hs
Compiling Data.String.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/String/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/String/Base.hs
Compiling Data.String.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/String/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/String/Properties.hs
Compiling Data.Char in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Char.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Char.hs
Compiling Data.String in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/String.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/String.hs
Compiling Agda.Builtin.Size in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Size.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Size.hs
Compiling Size in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Size.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Size.hs
Compiling Data.Maybe.Relation.Unary.All in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Maybe/Relation/Unary/All.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Maybe/Relation/Unary/All.hs
Compiling Data.List.Relation.Unary.All.Properties in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/List/Relation/Unary/All/Properties.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/List/Relation/Unary/All/Properties.hs
Compiling Data.Vec.Bounded.Base in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Vec/Bounded/Base.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Vec/Bounded/Base.hs
Compiling Data.Vec in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Vec.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Vec.hs
Compiling Data.Vec.Bounded in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Vec/Bounded.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Vec/Bounded.hs
Compiling Codata.Thunk in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Thunk.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Thunk.hs
Compiling Codata.Conat in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Conat.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Conat.hs
Compiling Codata.Delay in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Delay.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Delay.hs
Compiling Codata.Stream in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Stream.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Stream.hs
Compiling Data.BoundedVec.Inefficient in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/BoundedVec/Inefficient.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/BoundedVec/Inefficient.hs
Compiling Algebra.Properties.AbelianGroup in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/AbelianGroup.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/AbelianGroup.hs
Compiling Algebra.Properties.Ring in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/Ring.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/Ring.hs
Compiling Algebra.Solver.Ring.AlmostCommutativeRing in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Solver/Ring/AlmostCommutativeRing.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Solver/Ring/AlmostCommutativeRing.hs
Compiling Algebra.Definitions.RawMagma in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Definitions/RawMagma.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Definitions/RawMagma.hs
Compiling Data.Vec.Functional in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Vec/Functional.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Vec/Functional.hs
Compiling Algebra.Definitions.RawMonoid in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Definitions/RawMonoid.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Definitions/RawMonoid.hs
Compiling Algebra.Properties.Monoid.Mult in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/Monoid/Mult.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/Monoid/Mult.hs
Compiling Algebra.Definitions.RawSemiring in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Definitions/RawSemiring.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Definitions/RawSemiring.hs
Compiling Algebra.Properties.Semiring.Exp in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Properties/Semiring/Exp.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Properties/Semiring/Exp.hs
Compiling Data.Vec.N-ary in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Vec/N-ary.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Vec/NZ45Zary.hs
Compiling Relation.Binary.Reflection in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reflection.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reflection.hs
Compiling Algebra.Solver.Ring.Lemmas in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Solver/Ring/Lemmas.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Solver/Ring/Lemmas.hs
Compiling Algebra.Solver.Ring in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Solver/Ring.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Solver/Ring.hs
Compiling Algebra.Solver.Ring.Simple in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Algebra/Solver/Ring/Simple.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Algebra/Solver/Ring/Simple.hs
Compiling Data.Nat.Solver in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Nat/Solver.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Nat/Solver.hs
Compiling Data.BoundedVec in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/BoundedVec.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/BoundedVec.hs
Compiling Codata.Cowriter in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Cowriter.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Cowriter.hs
Compiling Codata.Colist in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Colist.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Colist.hs
Compiling Relation.Binary.Construct.FromRel in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Construct/FromRel.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Construct/FromRel.hs
Compiling Agda.Builtin.Coinduction in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/Coinduction.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/Coinduction.hs
Compiling Codata.Musical.Notation in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Musical/Notation.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Musical/Notation.hs
Compiling Codata.Musical.Conat in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Musical/Conat.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Musical/Conat.hs
Compiling Data.Maybe in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Data/Maybe.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Data/Maybe.hs
Compiling Relation.Binary.Reasoning.PartialOrder in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/PartialOrder.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/PartialOrder.hs
Compiling Relation.Binary.Reasoning.Base.Double in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/Base/Double.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/Base/Double.hs
Compiling Relation.Binary.Reasoning.Preorder in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Relation/Binary/Reasoning/Preorder.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Relation/Binary/Reasoning/Preorder.hs
Compiling Codata.Musical.Colist in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Musical/Colist.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Musical/Colist.hs
Compiling Codata.Musical.Costring in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/Codata/Musical/Costring.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Codata/Musical/Costring.hs
Compiling Agda.Builtin.IO in /usr/local/Cellar/agda/2.6.1.3/cabal/store/ghc-8.10.4/Agd-2.6.1.3-dd76333f/share/lib/prim/Agda/Builtin/IO.agdai to /Users/satnam/agda-examples/MAlonzo/Code/Agda/Builtin/IO.hs
Compiling IO.Primitive in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/IO/Primitive.agdai to /Users/satnam/agda-examples/MAlonzo/Code/IO/Primitive.hs
Compiling IO in /usr/local/Cellar/agda/2.6.1.3/lib/agda/_build/2.6.1.3/agda/src/IO.agdai to /Users/satnam/agda-examples/MAlonzo/Code/IO.hs
Compiling hello-world in /Users/satnam/agda-examples/hello-world.agdai to /Users/satnam/agda-examples/MAlonzo/Code/QhelloZ45Zworld.hs
Calling: ghc -O -o /Users/satnam/agda-examples/hello-world -Werror -i/Users/satnam/agda-examples -main-is MAlonzo.Code.QhelloZ45Zworld /Users/satnam/agda-examples/MAlonzo/Code/QhelloZ45Zworld.hs --make -fwarn-incomplete-patterns -fno-warn-overlapping-patterns
[  1 of 130] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
[  2 of 130] Compiling MAlonzo.Code.Agda.Primitive ( MAlonzo/Code/Agda/Primitive.hs, MAlonzo/Code/Agda/Primitive.o )
[  3 of 130] Compiling MAlonzo.Code.Level ( MAlonzo/Code/Level.hs, MAlonzo/Code/Level.o )
[  4 of 130] Compiling MAlonzo.Code.Data.Empty.Polymorphic ( MAlonzo/Code/Data/Empty/Polymorphic.hs, MAlonzo/Code/Data/Empty/Polymorphic.o )
[  5 of 130] Compiling MAlonzo.Code.Data.Empty ( MAlonzo/Code/Data/Empty.hs, MAlonzo/Code/Data/Empty.o )
[  6 of 130] Compiling MAlonzo.Code.Relation.Binary.Definitions ( MAlonzo/Code/Relation/Binary/Definitions.hs, MAlonzo/Code/Relation/Binary/Definitions.o )
[  7 of 130] Compiling MAlonzo.Code.Data.Empty.Irrelevant ( MAlonzo/Code/Data/Empty/Irrelevant.hs, MAlonzo/Code/Data/Empty/Irrelevant.o )
[  8 of 130] Compiling MAlonzo.Code.Relation.Nullary ( MAlonzo/Code/Relation/Nullary.hs, MAlonzo/Code/Relation/Nullary.o )
[  9 of 130] Compiling MAlonzo.Code.Agda.Builtin.Unit ( MAlonzo/Code/Agda/Builtin/Unit.hs, MAlonzo/Code/Agda/Builtin/Unit.o )
[ 10 of 130] Compiling MAlonzo.Code.Agda.Builtin.String ( MAlonzo/Code/Agda/Builtin/String.hs, MAlonzo/Code/Agda/Builtin/String.o )
[ 11 of 130] Compiling MAlonzo.Code.Agda.Builtin.Size ( MAlonzo/Code/Agda/Builtin/Size.hs, MAlonzo/Code/Agda/Builtin/Size.o )
[ 12 of 130] Compiling MAlonzo.Code.Codata.Thunk ( MAlonzo/Code/Codata/Thunk.hs, MAlonzo/Code/Codata/Thunk.o )
[ 13 of 130] Compiling MAlonzo.Code.Codata.Conat ( MAlonzo/Code/Codata/Conat.hs, MAlonzo/Code/Codata/Conat.o )
[ 14 of 130] Compiling MAlonzo.Code.Agda.Builtin.Sigma ( MAlonzo/Code/Agda/Builtin/Sigma.hs, MAlonzo/Code/Agda/Builtin/Sigma.o )
[ 15 of 130] Compiling MAlonzo.Code.Data.Product ( MAlonzo/Code/Data/Product.hs, MAlonzo/Code/Data/Product.o )
[ 16 of 130] Compiling MAlonzo.Code.Agda.Builtin.Nat ( MAlonzo/Code/Agda/Builtin/Nat.hs, MAlonzo/Code/Agda/Builtin/Nat.o )
[ 17 of 130] Compiling MAlonzo.Code.Agda.Builtin.List ( MAlonzo/Code/Agda/Builtin/List.hs, MAlonzo/Code/Agda/Builtin/List.o )
[ 18 of 130] Compiling MAlonzo.Code.Data.BoundedVec.Inefficient ( MAlonzo/Code/Data/BoundedVec/Inefficient.hs, MAlonzo/Code/Data/BoundedVec/Inefficient.o )
[ 19 of 130] Compiling MAlonzo.Code.Agda.Builtin.IO ( MAlonzo/Code/Agda/Builtin/IO.hs, MAlonzo/Code/Agda/Builtin/IO.o )
[ 20 of 130] Compiling MAlonzo.Code.Agda.Builtin.Equality ( MAlonzo/Code/Agda/Builtin/Equality.hs, MAlonzo/Code/Agda/Builtin/Equality.o )
[ 21 of 130] Compiling MAlonzo.Code.Relation.Nullary.Reflects ( MAlonzo/Code/Relation/Nullary/Reflects.hs, MAlonzo/Code/Relation/Nullary/Reflects.o )
[ 22 of 130] Compiling MAlonzo.Code.Relation.Binary.Reasoning.Base.Partial ( MAlonzo/Code/Relation/Binary/Reasoning/Base/Partial.hs, MAlonzo/Code/Relation/Binary/Reasoning/Base/Partial.o )
[ 23 of 130] Compiling MAlonzo.Code.Relation.Binary.PropositionalEquality.Core ( MAlonzo/Code/Relation/Binary/PropositionalEquality/Core.hs, MAlonzo/Code/Relation/Binary/PropositionalEquality/Core.o )
[ 24 of 130] Compiling MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures ( MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Structures.hs, MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Structures.o )
[ 25 of 130] Compiling MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles ( MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Bundles.hs, MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Bundles.o )
[ 26 of 130] Compiling MAlonzo.Code.Category.Functor ( MAlonzo/Code/Category/Functor.hs, MAlonzo/Code/Category/Functor.o )
[ 27 of 130] Compiling MAlonzo.Code.Category.Applicative.Indexed ( MAlonzo/Code/Category/Applicative/Indexed.hs, MAlonzo/Code/Category/Applicative/Indexed.o )
[ 28 of 130] Compiling MAlonzo.Code.Category.Monad.Indexed ( MAlonzo/Code/Category/Monad/Indexed.hs, MAlonzo/Code/Category/Monad/Indexed.o )
[ 29 of 130] Compiling MAlonzo.Code.Agda.Builtin.Coinduction ( MAlonzo/Code/Agda/Builtin/Coinduction.hs, MAlonzo/Code/Agda/Builtin/Coinduction.o )
[ 30 of 130] Compiling MAlonzo.Code.Agda.Builtin.Char ( MAlonzo/Code/Agda/Builtin/Char.hs, MAlonzo/Code/Agda/Builtin/Char.o )
[ 31 of 130] Compiling MAlonzo.Code.Agda.Builtin.Bool ( MAlonzo/Code/Agda/Builtin/Bool.hs, MAlonzo/Code/Agda/Builtin/Bool.o )
[ 32 of 130] Compiling MAlonzo.Code.Data.Sum.Base ( MAlonzo/Code/Data/Sum/Base.hs, MAlonzo/Code/Data/Sum/Base.o )
[ 33 of 130] Compiling MAlonzo.Code.Data.These.Base ( MAlonzo/Code/Data/These/Base.hs, MAlonzo/Code/Data/These/Base.o )
[ 34 of 130] Compiling MAlonzo.Code.Algebra.Consequences.Base ( MAlonzo/Code/Algebra/Consequences/Base.hs, MAlonzo/Code/Algebra/Consequences/Base.o )
[ 35 of 130] Compiling MAlonzo.Code.Data.Nat.Base ( MAlonzo/Code/Data/Nat/Base.hs, MAlonzo/Code/Data/Nat/Base.o )
[ 36 of 130] Compiling MAlonzo.Code.Data.Fin.Base ( MAlonzo/Code/Data/Fin/Base.hs, MAlonzo/Code/Data/Fin/Base.o )
[ 37 of 130] Compiling MAlonzo.Code.Data.Vec.Base ( MAlonzo/Code/Data/Vec/Base.hs, MAlonzo/Code/Data/Vec/Base.o )
[ 38 of 130] Compiling MAlonzo.Code.Data.Bool.Base ( MAlonzo/Code/Data/Bool/Base.hs, MAlonzo/Code/Data/Bool/Base.o )
[ 39 of 130] Compiling MAlonzo.Code.Relation.Nullary.Sum ( MAlonzo/Code/Relation/Nullary/Sum.hs, MAlonzo/Code/Relation/Nullary/Sum.o )
[ 40 of 130] Compiling MAlonzo.Code.Relation.Nullary.Product ( MAlonzo/Code/Relation/Nullary/Product.hs, MAlonzo/Code/Relation/Nullary/Product.o )
[ 41 of 130] Compiling MAlonzo.Code.Relation.Nullary.Decidable.Core ( MAlonzo/Code/Relation/Nullary/Decidable/Core.hs, MAlonzo/Code/Relation/Nullary/Decidable/Core.o )
[ 42 of 130] Compiling MAlonzo.Code.Relation.Nullary.Negation ( MAlonzo/Code/Relation/Nullary/Negation.hs, MAlonzo/Code/Relation/Nullary/Negation.o )
[ 43 of 130] Compiling MAlonzo.Code.Relation.Unary.Properties ( MAlonzo/Code/Relation/Unary/Properties.hs, MAlonzo/Code/Relation/Unary/Properties.o )
[ 44 of 130] Compiling MAlonzo.Code.Data.Maybe.Base ( MAlonzo/Code/Data/Maybe/Base.hs, MAlonzo/Code/Data/Maybe/Base.o )
[ 45 of 130] Compiling MAlonzo.Code.Relation.Binary.Consequences ( MAlonzo/Code/Relation/Binary/Consequences.hs, MAlonzo/Code/Relation/Binary/Consequences.o )
[ 46 of 130] Compiling MAlonzo.Code.Relation.Binary.Structures ( MAlonzo/Code/Relation/Binary/Structures.hs, MAlonzo/Code/Relation/Binary/Structures.o )
[ 47 of 130] Compiling MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple ( MAlonzo/Code/Relation/Binary/Reasoning/Base/Triple.hs, MAlonzo/Code/Relation/Binary/Reasoning/Base/Triple.o )
[ 48 of 130] Compiling MAlonzo.Code.Relation.Binary.Reasoning.Base.Double ( MAlonzo/Code/Relation/Binary/Reasoning/Base/Double.hs, MAlonzo/Code/Relation/Binary/Reasoning/Base/Double.o )
[ 49 of 130] Compiling MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict ( MAlonzo/Code/Relation/Binary/Construct/NonStrictToStrict.hs, MAlonzo/Code/Relation/Binary/Construct/NonStrictToStrict.o )
[ 50 of 130] Compiling MAlonzo.Code.Function.Metric.Structures ( MAlonzo/Code/Function/Metric/Structures.hs, MAlonzo/Code/Function/Metric/Structures.o )
[ 51 of 130] Compiling MAlonzo.Code.Function.Metric.Nat.Bundles ( MAlonzo/Code/Function/Metric/Nat/Bundles.hs, MAlonzo/Code/Function/Metric/Nat/Bundles.o )
[ 52 of 130] Compiling MAlonzo.Code.Relation.Binary.Bundles ( MAlonzo/Code/Relation/Binary/Bundles.hs, MAlonzo/Code/Relation/Binary/Bundles.o )
[ 53 of 130] Compiling MAlonzo.Code.Relation.Binary.Reasoning.PartialSetoid ( MAlonzo/Code/Relation/Binary/Reasoning/PartialSetoid.hs, MAlonzo/Code/Relation/Binary/Reasoning/PartialSetoid.o )
[ 54 of 130] Compiling MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties ( MAlonzo/Code/Relation/Binary/PropositionalEquality/Properties.hs, MAlonzo/Code/Relation/Binary/PropositionalEquality/Properties.o )
[ 55 of 130] Compiling MAlonzo.Code.Relation.Binary.Properties.Preorder ( MAlonzo/Code/Relation/Binary/Properties/Preorder.hs, MAlonzo/Code/Relation/Binary/Properties/Preorder.o )
[ 56 of 130] Compiling MAlonzo.Code.Relation.Binary.Properties.Poset ( MAlonzo/Code/Relation/Binary/Properties/Poset.hs, MAlonzo/Code/Relation/Binary/Properties/Poset.o )
[ 57 of 130] Compiling MAlonzo.Code.Relation.Binary.Lattice ( MAlonzo/Code/Relation/Binary/Lattice.hs, MAlonzo/Code/Relation/Binary/Lattice.o )
[ 58 of 130] Compiling MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Construct.Trivial ( MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.hs, MAlonzo/Code/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.o )
[ 59 of 130] Compiling MAlonzo.Code.Relation.Binary.Construct.FromRel ( MAlonzo/Code/Relation/Binary/Construct/FromRel.hs, MAlonzo/Code/Relation/Binary/Construct/FromRel.o )
[ 60 of 130] Compiling MAlonzo.Code.Relation.Binary.Construct.Converse ( MAlonzo/Code/Relation/Binary/Construct/Converse.hs, MAlonzo/Code/Relation/Binary/Construct/Converse.o )
[ 61 of 130] Compiling MAlonzo.Code.Function.Structures ( MAlonzo/Code/Function/Structures.hs, MAlonzo/Code/Function/Structures.o )
[ 62 of 130] Compiling MAlonzo.Code.Function.Equality ( MAlonzo/Code/Function/Equality.hs, MAlonzo/Code/Function/Equality.o )
[ 63 of 130] Compiling MAlonzo.Code.Relation.Binary.PropositionalEquality ( MAlonzo/Code/Relation/Binary/PropositionalEquality.hs, MAlonzo/Code/Relation/Binary/PropositionalEquality.o )
[ 64 of 130] Compiling MAlonzo.Code.Function.Injection ( MAlonzo/Code/Function/Injection.hs, MAlonzo/Code/Function/Injection.o )
[ 65 of 130] Compiling MAlonzo.Code.Function.Equivalence ( MAlonzo/Code/Function/Equivalence.hs, MAlonzo/Code/Function/Equivalence.o )
[ 66 of 130] Compiling MAlonzo.Code.Function.LeftInverse ( MAlonzo/Code/Function/LeftInverse.hs, MAlonzo/Code/Function/LeftInverse.o )
[ 67 of 130] Compiling MAlonzo.Code.Function.Surjection ( MAlonzo/Code/Function/Surjection.hs, MAlonzo/Code/Function/Surjection.o )
[ 68 of 130] Compiling MAlonzo.Code.Function.Bundles ( MAlonzo/Code/Function/Bundles.hs, MAlonzo/Code/Function/Bundles.o )
[ 69 of 130] Compiling MAlonzo.Code.Relation.Nullary.Decidable ( MAlonzo/Code/Relation/Nullary/Decidable.hs, MAlonzo/Code/Relation/Nullary/Decidable.o )
[ 70 of 130] Compiling MAlonzo.Code.Data.Product.Properties ( MAlonzo/Code/Data/Product/Properties.hs, MAlonzo/Code/Data/Product/Properties.o )
[ 71 of 130] Compiling MAlonzo.Code.Function.Bijection ( MAlonzo/Code/Function/Bijection.hs, MAlonzo/Code/Function/Bijection.o )
[ 72 of 130] Compiling MAlonzo.Code.Function.Inverse ( MAlonzo/Code/Function/Inverse.hs, MAlonzo/Code/Function/Inverse.o )
[ 73 of 130] Compiling MAlonzo.Code.Function.Related ( MAlonzo/Code/Function/Related.hs, MAlonzo/Code/Function/Related.o )
[ 74 of 130] Compiling MAlonzo.Code.Function.HalfAdjointEquivalence ( MAlonzo/Code/Function/HalfAdjointEquivalence.hs, MAlonzo/Code/Function/HalfAdjointEquivalence.o )
[ 75 of 130] Compiling MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise ( MAlonzo/Code/Data/Sum/Relation/Binary/Pointwise.hs, MAlonzo/Code/Data/Sum/Relation/Binary/Pointwise.o )
[ 76 of 130] Compiling MAlonzo.Code.Data.Sum.Function.Setoid ( MAlonzo/Code/Data/Sum/Function/Setoid.hs, MAlonzo/Code/Data/Sum/Function/Setoid.o )
[ 77 of 130] Compiling MAlonzo.Code.Data.Sum.Function.Propositional ( MAlonzo/Code/Data/Sum/Function/Propositional.hs, MAlonzo/Code/Data/Sum/Function/Propositional.o )
[ 78 of 130] Compiling MAlonzo.Code.Data.Product.Relation.Binary.Pointwise.NonDependent ( MAlonzo/Code/Data/Product/Relation/Binary/Pointwise/NonDependent.hs, MAlonzo/Code/Data/Product/Relation/Binary/Pointwise/NonDependent.o )
[ 79 of 130] Compiling MAlonzo.Code.Data.Product.Function.NonDependent.Setoid ( MAlonzo/Code/Data/Product/Function/NonDependent/Setoid.hs, MAlonzo/Code/Data/Product/Function/NonDependent/Setoid.o )
[ 80 of 130] Compiling MAlonzo.Code.Data.Product.Function.NonDependent.Propositional ( MAlonzo/Code/Data/Product/Function/NonDependent/Propositional.hs, MAlonzo/Code/Data/Product/Function/NonDependent/Propositional.o )
[ 81 of 130] Compiling MAlonzo.Code.Data.Product.Function.Dependent.Propositional ( MAlonzo/Code/Data/Product/Function/Dependent/Propositional.hs, MAlonzo/Code/Data/Product/Function/Dependent/Propositional.o )
[ 82 of 130] Compiling MAlonzo.Code.Codata.Musical.Conat ( MAlonzo/Code/Codata/Musical/Conat.hs, MAlonzo/Code/Codata/Musical/Conat.o )
[ 83 of 130] Compiling MAlonzo.Code.Algebra.Consequences.Setoid ( MAlonzo/Code/Algebra/Consequences/Setoid.hs, MAlonzo/Code/Algebra/Consequences/Setoid.o )
[ 84 of 130] Compiling MAlonzo.Code.Algebra.Structures ( MAlonzo/Code/Algebra/Structures.hs, MAlonzo/Code/Algebra/Structures.o )
[ 85 of 130] Compiling MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left ( MAlonzo/Code/Relation/Binary/Construct/NaturalOrder/Left.hs, MAlonzo/Code/Relation/Binary/Construct/NaturalOrder/Left.o )
[ 86 of 130] Compiling MAlonzo.Code.Algebra.Structures.Biased ( MAlonzo/Code/Algebra/Structures/Biased.hs, MAlonzo/Code/Algebra/Structures/Biased.o )
[ 87 of 130] Compiling MAlonzo.Code.Algebra.Construct.LiftedChoice ( MAlonzo/Code/Algebra/Construct/LiftedChoice.hs, MAlonzo/Code/Algebra/Construct/LiftedChoice.o )
[ 88 of 130] Compiling MAlonzo.Code.Algebra.Bundles ( MAlonzo/Code/Algebra/Bundles.hs, MAlonzo/Code/Algebra/Bundles.o )
[ 89 of 130] Compiling MAlonzo.Code.Relation.Binary.PropositionalEquality.Algebra ( MAlonzo/Code/Relation/Binary/PropositionalEquality/Algebra.hs, MAlonzo/Code/Relation/Binary/PropositionalEquality/Algebra.o )
[ 90 of 130] Compiling MAlonzo.Code.Function.Related.TypeIsomorphisms ( MAlonzo/Code/Function/Related/TypeIsomorphisms.hs, MAlonzo/Code/Function/Related/TypeIsomorphisms.o )
[ 91 of 130] Compiling MAlonzo.Code.Algebra.Properties.Semilattice ( MAlonzo/Code/Algebra/Properties/Semilattice.hs, MAlonzo/Code/Algebra/Properties/Semilattice.o )
[ 92 of 130] Compiling MAlonzo.Code.Algebra.Properties.Lattice ( MAlonzo/Code/Algebra/Properties/Lattice.hs, MAlonzo/Code/Algebra/Properties/Lattice.o )
[ 93 of 130] Compiling MAlonzo.Code.Algebra.Properties.DistributiveLattice ( MAlonzo/Code/Algebra/Properties/DistributiveLattice.hs, MAlonzo/Code/Algebra/Properties/DistributiveLattice.o )
[ 94 of 130] Compiling MAlonzo.Code.Algebra.Morphism ( MAlonzo/Code/Algebra/Morphism.hs, MAlonzo/Code/Algebra/Morphism.o )
[ 95 of 130] Compiling MAlonzo.Code.Algebra.Construct.NaturalChoice.Min ( MAlonzo/Code/Algebra/Construct/NaturalChoice/Min.hs, MAlonzo/Code/Algebra/Construct/NaturalChoice/Min.o )
[ 96 of 130] Compiling MAlonzo.Code.Data.List.Extrema.Core ( MAlonzo/Code/Data/List/Extrema/Core.hs, MAlonzo/Code/Data/List/Extrema/Core.o )
[ 97 of 130] Compiling MAlonzo.Code.Algebra.Properties.BooleanAlgebra ( MAlonzo/Code/Algebra/Properties/BooleanAlgebra.hs, MAlonzo/Code/Algebra/Properties/BooleanAlgebra.o )
[ 98 of 130] Compiling MAlonzo.Code.Data.Maybe.Relation.Unary.Any ( MAlonzo/Code/Data/Maybe/Relation/Unary/Any.hs, MAlonzo/Code/Data/Maybe/Relation/Unary/Any.o )
[ 99 of 130] Compiling MAlonzo.Code.Data.Maybe.Relation.Unary.All ( MAlonzo/Code/Data/Maybe/Relation/Unary/All.hs, MAlonzo/Code/Data/Maybe/Relation/Unary/All.o )
[100 of 130] Compiling MAlonzo.Code.Codata.Delay ( MAlonzo/Code/Codata/Delay.hs, MAlonzo/Code/Codata/Delay.o )
[101 of 130] Compiling MAlonzo.Code.Data.List.Base ( MAlonzo/Code/Data/List/Base.hs, MAlonzo/Code/Data/List/Base.o )
[102 of 130] Compiling MAlonzo.Code.Data.List.Relation.Unary.Any ( MAlonzo/Code/Data/List/Relation/Unary/Any.hs, MAlonzo/Code/Data/List/Relation/Unary/Any.o )
[103 of 130] Compiling MAlonzo.Code.Data.List.Relation.Unary.All ( MAlonzo/Code/Data/List/Relation/Unary/All.hs, MAlonzo/Code/Data/List/Relation/Unary/All.o )
[104 of 130] Compiling MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core ( MAlonzo/Code/Data/List/Relation/Unary/AllPairs/Core.hs, MAlonzo/Code/Data/List/Relation/Unary/AllPairs/Core.o )
[105 of 130] Compiling MAlonzo.Code.Data.List.Membership.Setoid ( MAlonzo/Code/Data/List/Membership/Setoid.hs, MAlonzo/Code/Data/List/Membership/Setoid.o )
[106 of 130] Compiling MAlonzo.Code.Data.List.Membership.Propositional ( MAlonzo/Code/Data/List/Membership/Propositional.hs, MAlonzo/Code/Data/List/Membership/Propositional.o )
[107 of 130] Compiling MAlonzo.Code.Data.List.Membership.Propositional.Properties.Core ( MAlonzo/Code/Data/List/Membership/Propositional/Properties/Core.hs, MAlonzo/Code/Data/List/Membership/Propositional/Properties/Core.o )
[108 of 130] Compiling MAlonzo.Code.Data.List.Categorical ( MAlonzo/Code/Data/List/Categorical.hs, MAlonzo/Code/Data/List/Categorical.o )
[109 of 130] Compiling MAlonzo.Code.Data.BoundedVec ( MAlonzo/Code/Data/BoundedVec.hs, MAlonzo/Code/Data/BoundedVec.o )
[110 of 130] Compiling MAlonzo.Code.Data.Bool.Properties ( MAlonzo/Code/Data/Bool/Properties.hs, MAlonzo/Code/Data/Bool/Properties.o )
[111 of 130] Compiling MAlonzo.Code.Data.Nat.Properties ( MAlonzo/Code/Data/Nat/Properties.hs, MAlonzo/Code/Data/Nat/Properties.o )
[112 of 130] Compiling MAlonzo.Code.Data.List.Properties ( MAlonzo/Code/Data/List/Properties.hs, MAlonzo/Code/Data/List/Properties.o )
[113 of 130] Compiling MAlonzo.Code.Data.List.Relation.Binary.Pointwise ( MAlonzo/Code/Data/List/Relation/Binary/Pointwise.hs, MAlonzo/Code/Data/List/Relation/Binary/Pointwise.o )
[114 of 130] Compiling MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid ( MAlonzo/Code/Data/List/Relation/Binary/Equality/Setoid.hs, MAlonzo/Code/Data/List/Relation/Binary/Equality/Setoid.o )
[115 of 130] Compiling MAlonzo.Code.Data.List.Relation.Binary.Equality.Propositional ( MAlonzo/Code/Data/List/Relation/Binary/Equality/Propositional.hs, MAlonzo/Code/Data/List/Relation/Binary/Equality/Propositional.o )
[116 of 130] Compiling MAlonzo.Code.Data.List.Relation.Unary.Any.Properties ( MAlonzo/Code/Data/List/Relation/Unary/Any/Properties.hs, MAlonzo/Code/Data/List/Relation/Unary/Any/Properties.o )
[117 of 130] Compiling MAlonzo.Code.Data.List.Membership.Setoid.Properties ( MAlonzo/Code/Data/List/Membership/Setoid/Properties.hs, MAlonzo/Code/Data/List/Membership/Setoid/Properties.o )
[118 of 130] Compiling MAlonzo.Code.Data.List.Membership.Propositional.Properties ( MAlonzo/Code/Data/List/Membership/Propositional/Properties.hs, MAlonzo/Code/Data/List/Membership/Propositional/Properties.o )
[119 of 130] Compiling MAlonzo.Code.Data.List.Extrema ( MAlonzo/Code/Data/List/Extrema.hs, MAlonzo/Code/Data/List/Extrema.o )
[120 of 130] Compiling MAlonzo.Code.Data.List.Relation.Unary.All.Properties ( MAlonzo/Code/Data/List/Relation/Unary/All/Properties.hs, MAlonzo/Code/Data/List/Relation/Unary/All/Properties.o )
[121 of 130] Compiling MAlonzo.Code.Data.Vec.Bounded.Base ( MAlonzo/Code/Data/Vec/Bounded/Base.hs, MAlonzo/Code/Data/Vec/Bounded/Base.o )
[122 of 130] Compiling MAlonzo.Code.Data.List.NonEmpty ( MAlonzo/Code/Data/List/NonEmpty.hs, MAlonzo/Code/Data/List/NonEmpty.o )
[123 of 130] Compiling MAlonzo.Code.Codata.Stream ( MAlonzo/Code/Codata/Stream.hs, MAlonzo/Code/Codata/Stream.o )
[124 of 130] Compiling MAlonzo.Code.Codata.Cowriter ( MAlonzo/Code/Codata/Cowriter.hs, MAlonzo/Code/Codata/Cowriter.o )
[125 of 130] Compiling MAlonzo.Code.Codata.Colist ( MAlonzo/Code/Codata/Colist.hs, MAlonzo/Code/Codata/Colist.o )
[126 of 130] Compiling MAlonzo.Code.Codata.Musical.Colist ( MAlonzo/Code/Codata/Musical/Colist.hs, MAlonzo/Code/Codata/Musical/Colist.o )
[127 of 130] Compiling MAlonzo.Code.IO.Primitive ( MAlonzo/Code/IO/Primitive.hs, MAlonzo/Code/IO/Primitive.o )
[128 of 130] Compiling MAlonzo.Code.Codata.Musical.Costring ( MAlonzo/Code/Codata/Musical/Costring.hs, MAlonzo/Code/Codata/Musical/Costring.o )
[129 of 130] Compiling MAlonzo.Code.IO  ( MAlonzo/Code/IO.hs, MAlonzo/Code/IO.o )
[130 of 130] Compiling MAlonzo.Code.QhelloZ45Zworld ( /Users/satnam/agda-examples/MAlonzo/Code/QhelloZ45Zworld.hs, /Users/satnam/agda-examples/MAlonzo/Code/QhelloZ45Zworld.o )
Linking /Users/satnam/agda-examples/hello-world ...
satnam-macbookpro3:agda-examples satnam$ ./hello-world
Hello, World!

Good point. I have a patch to take this down to 34 modules. I'll open a PR tomorrow.

Was this page helpful?
0 / 5 - 0 ratings