diff --git a/Agda.Builtin.Bool.html b/Agda.Builtin.Bool.html index d66fa1a..4b7d192 100644 --- a/Agda.Builtin.Bool.html +++ b/Agda.Builtin.Bool.html @@ -1,5 +1,5 @@ -
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism +Agda.Builtin.Bool Source code on Github{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Bool where diff --git a/Agda.Builtin.Char.Properties.html b/Agda.Builtin.Char.Properties.html index abd831b..2445bea 100644 --- a/Agda.Builtin.Char.Properties.html +++ b/Agda.Builtin.Char.Properties.html @@ -1,5 +1,5 @@ -Agda.Builtin.Char.Properties Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} +Agda.Builtin.Char.Properties Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Char.Properties where diff --git a/Agda.Builtin.Char.html b/Agda.Builtin.Char.html index d200775..3de6831 100644 --- a/Agda.Builtin.Char.html +++ b/Agda.Builtin.Char.html @@ -1,5 +1,5 @@ -Agda.Builtin.Char Source code on Github{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism +Agda.Builtin.Char Source code on Github{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Char where diff --git a/Agda.Builtin.Equality.html b/Agda.Builtin.Equality.html index 2507163..eab64ec 100644 --- a/Agda.Builtin.Equality.html +++ b/Agda.Builtin.Equality.html @@ -1,5 +1,5 @@ -Agda.Builtin.Equality Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} +Agda.Builtin.Equality Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Equality where diff --git a/Agda.Builtin.Float.Properties.html b/Agda.Builtin.Float.Properties.html index d12a6ed..a5984ed 100644 --- a/Agda.Builtin.Float.Properties.html +++ b/Agda.Builtin.Float.Properties.html @@ -1,5 +1,5 @@ -Agda.Builtin.Float.Properties Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} +Agda.Builtin.Float.Properties Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Float.Properties where diff --git a/Agda.Builtin.Float.html b/Agda.Builtin.Float.html index dcba085..95b5821 100644 --- a/Agda.Builtin.Float.html +++ b/Agda.Builtin.Float.html @@ -1,5 +1,5 @@ -Agda.Builtin.Float Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} +Agda.Builtin.Float Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Float where diff --git a/Agda.Builtin.Int.html b/Agda.Builtin.Int.html index 8c545c4..6bc7d5b 100644 --- a/Agda.Builtin.Int.html +++ b/Agda.Builtin.Int.html @@ -1,5 +1,5 @@ -Agda.Builtin.Int Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} +Agda.Builtin.Int Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Int where diff --git a/Agda.Builtin.List.html b/Agda.Builtin.List.html index 4424fc7..2691cd1 100644 --- a/Agda.Builtin.List.html +++ b/Agda.Builtin.List.html @@ -1,5 +1,5 @@ -Agda.Builtin.List Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} +Agda.Builtin.List Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.List where diff --git a/Agda.Builtin.Maybe.html b/Agda.Builtin.Maybe.html index 8751b75..880e3cd 100644 --- a/Agda.Builtin.Maybe.html +++ b/Agda.Builtin.Maybe.html @@ -1,5 +1,5 @@ -Agda.Builtin.Maybe Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} +Agda.Builtin.Maybe Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Maybe where diff --git a/Agda.Builtin.Nat.html b/Agda.Builtin.Nat.html index 62a67fd..db66d14 100644 --- a/Agda.Builtin.Nat.html +++ b/Agda.Builtin.Nat.html @@ -1,5 +1,5 @@ -Agda.Builtin.Nat Source code on Github{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism +Agda.Builtin.Nat Source code on Github{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Nat where diff --git a/Agda.Builtin.Reflection.Properties.html b/Agda.Builtin.Reflection.Properties.html index ff80d80..cb83668 100644 --- a/Agda.Builtin.Reflection.Properties.html +++ b/Agda.Builtin.Reflection.Properties.html @@ -1,5 +1,5 @@ -Agda.Builtin.Reflection.Properties Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} +Agda.Builtin.Reflection.Properties Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Reflection.Properties where diff --git a/Agda.Builtin.Reflection.html b/Agda.Builtin.Reflection.html index 93df546..c335808 100644 --- a/Agda.Builtin.Reflection.html +++ b/Agda.Builtin.Reflection.html @@ -1,5 +1,5 @@ -Agda.Builtin.Reflection Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} +Agda.Builtin.Reflection Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Reflection where diff --git a/Agda.Builtin.Sigma.html b/Agda.Builtin.Sigma.html index d0a36bd..167581f 100644 --- a/Agda.Builtin.Sigma.html +++ b/Agda.Builtin.Sigma.html @@ -1,5 +1,5 @@ -Agda.Builtin.Sigma Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} +Agda.Builtin.Sigma Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Sigma where diff --git a/Agda.Builtin.Strict.html b/Agda.Builtin.Strict.html index c68ac5c..01bc5d2 100644 --- a/Agda.Builtin.Strict.html +++ b/Agda.Builtin.Strict.html @@ -1,5 +1,5 @@ -Agda.Builtin.Strict Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} +Agda.Builtin.Strict Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Strict where diff --git a/Agda.Builtin.String.Properties.html b/Agda.Builtin.String.Properties.html index e05651d..15d63f1 100644 --- a/Agda.Builtin.String.Properties.html +++ b/Agda.Builtin.String.Properties.html @@ -1,5 +1,5 @@ -Agda.Builtin.String.Properties Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} +Agda.Builtin.String.Properties Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.String.Properties where diff --git a/Agda.Builtin.String.html b/Agda.Builtin.String.html index a7f2284..253662c 100644 --- a/Agda.Builtin.String.html +++ b/Agda.Builtin.String.html @@ -1,5 +1,5 @@ -Agda.Builtin.String Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} +Agda.Builtin.String Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.String where diff --git a/Agda.Builtin.Unit.html b/Agda.Builtin.Unit.html index 43d04bf..5075c9c 100644 --- a/Agda.Builtin.Unit.html +++ b/Agda.Builtin.Unit.html @@ -1,5 +1,5 @@ -Agda.Builtin.Unit Source code on Github{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism +Agda.Builtin.Unit Source code on Github{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Unit where diff --git a/Agda.Builtin.Word.Properties.html b/Agda.Builtin.Word.Properties.html index 763447c..a043e08 100644 --- a/Agda.Builtin.Word.Properties.html +++ b/Agda.Builtin.Word.Properties.html @@ -1,5 +1,5 @@ -Agda.Builtin.Word.Properties Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} +Agda.Builtin.Word.Properties Source code on Github{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Word.Properties where diff --git a/Agda.Builtin.Word.html b/Agda.Builtin.Word.html index fe7bcab..8454fe0 100644 --- a/Agda.Builtin.Word.html +++ b/Agda.Builtin.Word.html @@ -1,5 +1,5 @@ -Agda.Builtin.Word Source code on Github{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism +Agda.Builtin.Word Source code on Github{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Word where diff --git a/Agda.Primitive.html b/Agda.Primitive.html index 9ad88ae..aa10301 100644 --- a/Agda.Primitive.html +++ b/Agda.Primitive.html @@ -1,5 +1,5 @@ -Agda.Primitive Source code on Github-- The Agda primitives (preloaded). +Agda.Primitive Source code on Github-- The Agda primitives (preloaded). {-# OPTIONS --cubical-compatible --no-import-sorts --level-universe #-} diff --git a/Algebra.Apartness.Bundles.html b/Algebra.Apartness.Bundles.html index b7fcac6..dbe3791 100644 --- a/Algebra.Apartness.Bundles.html +++ b/Algebra.Apartness.Bundles.html @@ -1,5 +1,5 @@ -Algebra.Apartness.Bundles Source code on Github------------------------------------------------------------------------ +Algebra.Apartness.Bundles Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Bundles for local algebraic structures diff --git a/Algebra.Apartness.Structures.html b/Algebra.Apartness.Structures.html index 1a56f04..c953d3e 100644 --- a/Algebra.Apartness.Structures.html +++ b/Algebra.Apartness.Structures.html @@ -1,5 +1,5 @@ -Algebra.Apartness.Structures Source code on Github------------------------------------------------------------------------ +Algebra.Apartness.Structures Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Algebraic structures with an apartness relation diff --git a/Algebra.Apartness.html b/Algebra.Apartness.html index 2089775..aa73711 100644 --- a/Algebra.Apartness.html +++ b/Algebra.Apartness.html @@ -1,5 +1,5 @@ -Algebra.Apartness Source code on Github------------------------------------------------------------------------ +Algebra.Apartness Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Algebraic objects with an apartness relation diff --git a/Algebra.Bundles.Raw.html b/Algebra.Bundles.Raw.html index 9f3a275..2f3b64b 100644 --- a/Algebra.Bundles.Raw.html +++ b/Algebra.Bundles.Raw.html @@ -1,5 +1,5 @@ -Algebra.Bundles.Raw Source code on Github------------------------------------------------------------------------ +Algebra.Bundles.Raw Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Definitions of 'raw' bundles diff --git a/Algebra.Bundles.html b/Algebra.Bundles.html index a6efbe3..f87f8e9 100644 --- a/Algebra.Bundles.html +++ b/Algebra.Bundles.html @@ -1,5 +1,5 @@ -Algebra.Bundles Source code on Github------------------------------------------------------------------------ +Algebra.Bundles Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Definitions of algebraic structures like monoids and rings diff --git a/Algebra.Consequences.Base.html b/Algebra.Consequences.Base.html index 0e1a5c2..bba5612 100644 --- a/Algebra.Consequences.Base.html +++ b/Algebra.Consequences.Base.html @@ -1,5 +1,5 @@ -Algebra.Consequences.Base Source code on Github------------------------------------------------------------------------ +Algebra.Consequences.Base Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Lemmas relating algebraic definitions (such as associativity and diff --git a/Algebra.Consequences.Propositional.html b/Algebra.Consequences.Propositional.html index a6dfa06..86bb363 100644 --- a/Algebra.Consequences.Propositional.html +++ b/Algebra.Consequences.Propositional.html @@ -1,5 +1,5 @@ -Algebra.Consequences.Propositional Source code on Github------------------------------------------------------------------------ +Algebra.Consequences.Propositional Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Relations between properties of functions, such as associativity and diff --git a/Algebra.Consequences.Setoid.html b/Algebra.Consequences.Setoid.html index 3b7dda6..25c60e3 100644 --- a/Algebra.Consequences.Setoid.html +++ b/Algebra.Consequences.Setoid.html @@ -1,5 +1,5 @@ -Algebra.Consequences.Setoid Source code on Github------------------------------------------------------------------------ +Algebra.Consequences.Setoid Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Relations between properties of functions, such as associativity and diff --git a/Algebra.Construct.LiftedChoice.html b/Algebra.Construct.LiftedChoice.html index d80860d..010936c 100644 --- a/Algebra.Construct.LiftedChoice.html +++ b/Algebra.Construct.LiftedChoice.html @@ -1,5 +1,5 @@ -Algebra.Construct.LiftedChoice Source code on Github------------------------------------------------------------------------ +Algebra.Construct.LiftedChoice Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Choosing between elements based on the result of applying a function diff --git a/Algebra.Construct.NaturalChoice.Base.html b/Algebra.Construct.NaturalChoice.Base.html index 2e6008b..0f4bd5d 100644 --- a/Algebra.Construct.NaturalChoice.Base.html +++ b/Algebra.Construct.NaturalChoice.Base.html @@ -1,5 +1,5 @@ -Algebra.Construct.NaturalChoice.Base Source code on Github------------------------------------------------------------------------ +Algebra.Construct.NaturalChoice.Base Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Basic definition of an operator that computes the min/max value diff --git a/Algebra.Construct.NaturalChoice.Max.html b/Algebra.Construct.NaturalChoice.Max.html index 52c9780..49760f4 100644 --- a/Algebra.Construct.NaturalChoice.Max.html +++ b/Algebra.Construct.NaturalChoice.Max.html @@ -1,5 +1,5 @@ -Algebra.Construct.NaturalChoice.Max Source code on Github------------------------------------------------------------------------ +Algebra.Construct.NaturalChoice.Max Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- The max operator derived from an arbitrary total preorder. diff --git a/Algebra.Construct.NaturalChoice.MaxOp.html b/Algebra.Construct.NaturalChoice.MaxOp.html index d1ed4b3..275ea24 100644 --- a/Algebra.Construct.NaturalChoice.MaxOp.html +++ b/Algebra.Construct.NaturalChoice.MaxOp.html @@ -1,5 +1,5 @@ -Algebra.Construct.NaturalChoice.MaxOp Source code on Github------------------------------------------------------------------------ +Algebra.Construct.NaturalChoice.MaxOp Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of a max operator derived from a spec over a total diff --git a/Algebra.Construct.NaturalChoice.Min.html b/Algebra.Construct.NaturalChoice.Min.html index af51d85..44f783b 100644 --- a/Algebra.Construct.NaturalChoice.Min.html +++ b/Algebra.Construct.NaturalChoice.Min.html @@ -1,5 +1,5 @@ -Algebra.Construct.NaturalChoice.Min Source code on Github------------------------------------------------------------------------ +Algebra.Construct.NaturalChoice.Min Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- The min operator derived from an arbitrary total preorder. diff --git a/Algebra.Construct.NaturalChoice.MinMaxOp.html b/Algebra.Construct.NaturalChoice.MinMaxOp.html index 47d603c..390ac5a 100644 --- a/Algebra.Construct.NaturalChoice.MinMaxOp.html +++ b/Algebra.Construct.NaturalChoice.MinMaxOp.html @@ -1,5 +1,5 @@ -Algebra.Construct.NaturalChoice.MinMaxOp Source code on Github------------------------------------------------------------------------ +Algebra.Construct.NaturalChoice.MinMaxOp Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of min and max operators specified over a total diff --git a/Algebra.Construct.NaturalChoice.MinOp.html b/Algebra.Construct.NaturalChoice.MinOp.html index 470c7c6..6c29ccf 100644 --- a/Algebra.Construct.NaturalChoice.MinOp.html +++ b/Algebra.Construct.NaturalChoice.MinOp.html @@ -1,5 +1,5 @@ -Algebra.Construct.NaturalChoice.MinOp Source code on Github------------------------------------------------------------------------ +Algebra.Construct.NaturalChoice.MinOp Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of a min operator derived from a spec over a total diff --git a/Algebra.Core.html b/Algebra.Core.html index fbfe03f..085a919 100644 --- a/Algebra.Core.html +++ b/Algebra.Core.html @@ -1,5 +1,5 @@ -Algebra.Core Source code on Github------------------------------------------------------------------------ +Algebra.Core Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Core algebraic definitions diff --git a/Algebra.Definitions.RawMagma.html b/Algebra.Definitions.RawMagma.html index c5c7444..8ec888d 100644 --- a/Algebra.Definitions.RawMagma.html +++ b/Algebra.Definitions.RawMagma.html @@ -1,5 +1,5 @@ -Algebra.Definitions.RawMagma Source code on Github------------------------------------------------------------------------ +Algebra.Definitions.RawMagma Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Basic auxiliary definitions for magma-like structures diff --git a/Algebra.Definitions.RawMonoid.html b/Algebra.Definitions.RawMonoid.html index 76f1aa3..1d21fb4 100644 --- a/Algebra.Definitions.RawMonoid.html +++ b/Algebra.Definitions.RawMonoid.html @@ -1,5 +1,5 @@ -Algebra.Definitions.RawMonoid Source code on Github------------------------------------------------------------------------ +Algebra.Definitions.RawMonoid Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Basic auxiliary definitions for monoid-like structures diff --git a/Algebra.Definitions.RawSemiring.html b/Algebra.Definitions.RawSemiring.html index 76a5c9f..60c960b 100644 --- a/Algebra.Definitions.RawSemiring.html +++ b/Algebra.Definitions.RawSemiring.html @@ -1,5 +1,5 @@ -Algebra.Definitions.RawSemiring Source code on Github------------------------------------------------------------------------ +Algebra.Definitions.RawSemiring Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Basic auxiliary definitions for semiring-like structures diff --git a/Algebra.Definitions.html b/Algebra.Definitions.html index a94071e..ac5373e 100644 --- a/Algebra.Definitions.html +++ b/Algebra.Definitions.html @@ -1,5 +1,5 @@ -Algebra.Definitions Source code on Github------------------------------------------------------------------------ +Algebra.Definitions Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of functions, such as associativity and commutativity diff --git a/Algebra.Function.html b/Algebra.Function.html index 48df84c..a8470f2 100644 --- a/Algebra.Function.html +++ b/Algebra.Function.html @@ -1,5 +1,5 @@ -Algebra.Function Source code on Github{-# OPTIONS --safe --without-K #-} +Algebra.Function Source code on Github{-# OPTIONS --safe --without-K #-} open import Level open import Algebra.Lattice diff --git a/Algebra.Lattice.Bundles.Raw.html b/Algebra.Lattice.Bundles.Raw.html index c26ed61..a79c24d 100644 --- a/Algebra.Lattice.Bundles.Raw.html +++ b/Algebra.Lattice.Bundles.Raw.html @@ -1,5 +1,5 @@ -Algebra.Lattice.Bundles.Raw Source code on Github------------------------------------------------------------------------ +Algebra.Lattice.Bundles.Raw Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Definitions of 'raw' bundles diff --git a/Algebra.Lattice.Bundles.html b/Algebra.Lattice.Bundles.html index 67a314f..74166c7 100644 --- a/Algebra.Lattice.Bundles.html +++ b/Algebra.Lattice.Bundles.html @@ -1,5 +1,5 @@ -Algebra.Lattice.Bundles Source code on Github------------------------------------------------------------------------ +Algebra.Lattice.Bundles Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Definitions of algebraic structures like semilattices and lattices diff --git a/Algebra.Lattice.Construct.NaturalChoice.MaxOp.html b/Algebra.Lattice.Construct.NaturalChoice.MaxOp.html index dfe877e..0dbd754 100644 --- a/Algebra.Lattice.Construct.NaturalChoice.MaxOp.html +++ b/Algebra.Lattice.Construct.NaturalChoice.MaxOp.html @@ -1,5 +1,5 @@ -Algebra.Lattice.Construct.NaturalChoice.MaxOp Source code on Github------------------------------------------------------------------------ +Algebra.Lattice.Construct.NaturalChoice.MaxOp Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of a max operator derived from a spec over a total diff --git a/Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.html b/Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.html index 353d2c4..38404ab 100644 --- a/Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.html +++ b/Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.html @@ -1,5 +1,5 @@ -Algebra.Lattice.Construct.NaturalChoice.MinMaxOp Source code on Github------------------------------------------------------------------------ +Algebra.Lattice.Construct.NaturalChoice.MinMaxOp Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of min and max operators specified over a total preorder. diff --git a/Algebra.Lattice.Construct.NaturalChoice.MinOp.html b/Algebra.Lattice.Construct.NaturalChoice.MinOp.html index 8dc0456..cb4031b 100644 --- a/Algebra.Lattice.Construct.NaturalChoice.MinOp.html +++ b/Algebra.Lattice.Construct.NaturalChoice.MinOp.html @@ -1,5 +1,5 @@ -Algebra.Lattice.Construct.NaturalChoice.MinOp Source code on Github------------------------------------------------------------------------ +Algebra.Lattice.Construct.NaturalChoice.MinOp Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of a min operator derived from a spec over a total diff --git a/Algebra.Lattice.Morphism.LatticeMonomorphism.html b/Algebra.Lattice.Morphism.LatticeMonomorphism.html index d202da7..7656f01 100644 --- a/Algebra.Lattice.Morphism.LatticeMonomorphism.html +++ b/Algebra.Lattice.Morphism.LatticeMonomorphism.html @@ -1,5 +1,5 @@ -Algebra.Lattice.Morphism.LatticeMonomorphism Source code on Github------------------------------------------------------------------------ +Algebra.Lattice.Morphism.LatticeMonomorphism Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Consequences of a monomorphism between lattice-like structures diff --git a/Algebra.Lattice.Morphism.Structures.html b/Algebra.Lattice.Morphism.Structures.html index 5678d61..af4be53 100644 --- a/Algebra.Lattice.Morphism.Structures.html +++ b/Algebra.Lattice.Morphism.Structures.html @@ -1,5 +1,5 @@ -Algebra.Lattice.Morphism.Structures Source code on Github------------------------------------------------------------------------ +Algebra.Lattice.Morphism.Structures Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Morphisms between algebraic lattice structures diff --git a/Algebra.Lattice.Properties.BooleanAlgebra.html b/Algebra.Lattice.Properties.BooleanAlgebra.html index 0a2ed82..ede3f4a 100644 --- a/Algebra.Lattice.Properties.BooleanAlgebra.html +++ b/Algebra.Lattice.Properties.BooleanAlgebra.html @@ -1,5 +1,5 @@ -Algebra.Lattice.Properties.BooleanAlgebra Source code on Github------------------------------------------------------------------------ +Algebra.Lattice.Properties.BooleanAlgebra Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some derivable properties of Boolean algebras diff --git a/Algebra.Lattice.Properties.DistributiveLattice.html b/Algebra.Lattice.Properties.DistributiveLattice.html index e7f0a7b..de578b2 100644 --- a/Algebra.Lattice.Properties.DistributiveLattice.html +++ b/Algebra.Lattice.Properties.DistributiveLattice.html @@ -1,5 +1,5 @@ -Algebra.Lattice.Properties.DistributiveLattice Source code on Github------------------------------------------------------------------------ +Algebra.Lattice.Properties.DistributiveLattice Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some derivable properties diff --git a/Algebra.Lattice.Properties.Lattice.html b/Algebra.Lattice.Properties.Lattice.html index c2e0820..5dd6358 100644 --- a/Algebra.Lattice.Properties.Lattice.html +++ b/Algebra.Lattice.Properties.Lattice.html @@ -1,5 +1,5 @@ -Algebra.Lattice.Properties.Lattice Source code on Github------------------------------------------------------------------------ +Algebra.Lattice.Properties.Lattice Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some derivable properties of lattices diff --git a/Algebra.Lattice.Properties.Semilattice.html b/Algebra.Lattice.Properties.Semilattice.html index 7f52aa6..7d747c0 100644 --- a/Algebra.Lattice.Properties.Semilattice.html +++ b/Algebra.Lattice.Properties.Semilattice.html @@ -1,5 +1,5 @@ -Algebra.Lattice.Properties.Semilattice Source code on Github------------------------------------------------------------------------ +Algebra.Lattice.Properties.Semilattice Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some derivable properties of semilattices diff --git a/Algebra.Lattice.Structures.Biased.html b/Algebra.Lattice.Structures.Biased.html index e873799..4bef223 100644 --- a/Algebra.Lattice.Structures.Biased.html +++ b/Algebra.Lattice.Structures.Biased.html @@ -1,5 +1,5 @@ -Algebra.Lattice.Structures.Biased Source code on Github------------------------------------------------------------------------ +Algebra.Lattice.Structures.Biased Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some biased records for lattice-like structures. Such records are diff --git a/Algebra.Lattice.Structures.html b/Algebra.Lattice.Structures.html index d603335..3878500 100644 --- a/Algebra.Lattice.Structures.html +++ b/Algebra.Lattice.Structures.html @@ -1,5 +1,5 @@ -Algebra.Lattice.Structures Source code on Github------------------------------------------------------------------------ +Algebra.Lattice.Structures Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some lattice-like structures defined by properties of _∧_ and _∨_ diff --git a/Algebra.Lattice.html b/Algebra.Lattice.html index ed0e5b7..2c4a0f2 100644 --- a/Algebra.Lattice.html +++ b/Algebra.Lattice.html @@ -1,5 +1,5 @@ -Algebra.Lattice Source code on Github------------------------------------------------------------------------ +Algebra.Lattice Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Definitions of algebraic structures like semilattices and lattices diff --git a/Algebra.Morphism.Definitions.html b/Algebra.Morphism.Definitions.html index 8cc4100..0c12dca 100644 --- a/Algebra.Morphism.Definitions.html +++ b/Algebra.Morphism.Definitions.html @@ -1,5 +1,5 @@ -Algebra.Morphism.Definitions Source code on Github------------------------------------------------------------------------ +Algebra.Morphism.Definitions Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Basic definitions for morphisms between algebraic structures diff --git a/Algebra.Morphism.GroupMonomorphism.html b/Algebra.Morphism.GroupMonomorphism.html index 67ec315..08c3295 100644 --- a/Algebra.Morphism.GroupMonomorphism.html +++ b/Algebra.Morphism.GroupMonomorphism.html @@ -1,5 +1,5 @@ -Algebra.Morphism.GroupMonomorphism Source code on Github------------------------------------------------------------------------ +Algebra.Morphism.GroupMonomorphism Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Consequences of a monomorphism between group-like structures diff --git a/Algebra.Morphism.MagmaMonomorphism.html b/Algebra.Morphism.MagmaMonomorphism.html index 00c1699..91368d8 100644 --- a/Algebra.Morphism.MagmaMonomorphism.html +++ b/Algebra.Morphism.MagmaMonomorphism.html @@ -1,5 +1,5 @@ -Algebra.Morphism.MagmaMonomorphism Source code on Github------------------------------------------------------------------------ +Algebra.Morphism.MagmaMonomorphism Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Consequences of a monomorphism between magma-like structures diff --git a/Algebra.Morphism.MonoidMonomorphism.html b/Algebra.Morphism.MonoidMonomorphism.html index 77a6291..1775b07 100644 --- a/Algebra.Morphism.MonoidMonomorphism.html +++ b/Algebra.Morphism.MonoidMonomorphism.html @@ -1,5 +1,5 @@ -Algebra.Morphism.MonoidMonomorphism Source code on Github------------------------------------------------------------------------ +Algebra.Morphism.MonoidMonomorphism Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Consequences of a monomorphism between monoid-like structures diff --git a/Algebra.Morphism.RingMonomorphism.html b/Algebra.Morphism.RingMonomorphism.html index 1e471bf..019de62 100644 --- a/Algebra.Morphism.RingMonomorphism.html +++ b/Algebra.Morphism.RingMonomorphism.html @@ -1,5 +1,5 @@ -Algebra.Morphism.RingMonomorphism Source code on Github------------------------------------------------------------------------ +Algebra.Morphism.RingMonomorphism Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Consequences of a monomorphism between ring-like structures diff --git a/Algebra.Morphism.Structures.html b/Algebra.Morphism.Structures.html index ed73895..84ad04c 100644 --- a/Algebra.Morphism.Structures.html +++ b/Algebra.Morphism.Structures.html @@ -1,5 +1,5 @@ -Algebra.Morphism.Structures Source code on Github------------------------------------------------------------------------ +Algebra.Morphism.Structures Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Morphisms between algebraic structures diff --git a/Algebra.Morphism.html b/Algebra.Morphism.html index c860c3d..79dcd11 100644 --- a/Algebra.Morphism.html +++ b/Algebra.Morphism.html @@ -1,5 +1,5 @@ -Algebra.Morphism Source code on Github------------------------------------------------------------------------ +Algebra.Morphism Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Morphisms between algebraic structures diff --git a/Algebra.Properties.AbelianGroup.html b/Algebra.Properties.AbelianGroup.html index 79eb84d..de75781 100644 --- a/Algebra.Properties.AbelianGroup.html +++ b/Algebra.Properties.AbelianGroup.html @@ -1,5 +1,5 @@ -Algebra.Properties.AbelianGroup Source code on Github------------------------------------------------------------------------ +Algebra.Properties.AbelianGroup Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some derivable properties diff --git a/Algebra.Properties.CommutativeSemigroup.html b/Algebra.Properties.CommutativeSemigroup.html index 2b6eee3..f79f93b 100644 --- a/Algebra.Properties.CommutativeSemigroup.html +++ b/Algebra.Properties.CommutativeSemigroup.html @@ -1,5 +1,5 @@ -Algebra.Properties.CommutativeSemigroup Source code on Github------------------------------------------------------------------------ +Algebra.Properties.CommutativeSemigroup Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some theory for commutative semigroup diff --git a/Algebra.Properties.Group.html b/Algebra.Properties.Group.html index 34e6c05..b4d380d 100644 --- a/Algebra.Properties.Group.html +++ b/Algebra.Properties.Group.html @@ -1,5 +1,5 @@ -Algebra.Properties.Group Source code on Github------------------------------------------------------------------------ +Algebra.Properties.Group Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some derivable properties diff --git a/Algebra.Properties.Loop.html b/Algebra.Properties.Loop.html index 256d9e7..9f00ea8 100644 --- a/Algebra.Properties.Loop.html +++ b/Algebra.Properties.Loop.html @@ -1,5 +1,5 @@ -Algebra.Properties.Loop Source code on Github------------------------------------------------------------------------ +Algebra.Properties.Loop Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some basic properties of Loop diff --git a/Algebra.Properties.Monoid.Mult.html b/Algebra.Properties.Monoid.Mult.html index 6baa05d..ab2f3f2 100644 --- a/Algebra.Properties.Monoid.Mult.html +++ b/Algebra.Properties.Monoid.Mult.html @@ -1,5 +1,5 @@ -Algebra.Properties.Monoid.Mult Source code on Github------------------------------------------------------------------------ +Algebra.Properties.Monoid.Mult Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Multiplication over a monoid (i.e. repeated addition) diff --git a/Algebra.Properties.Quasigroup.html b/Algebra.Properties.Quasigroup.html index d130a9b..6ee306e 100644 --- a/Algebra.Properties.Quasigroup.html +++ b/Algebra.Properties.Quasigroup.html @@ -1,5 +1,5 @@ -Algebra.Properties.Quasigroup Source code on Github------------------------------------------------------------------------ +Algebra.Properties.Quasigroup Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some basic properties of Quasigroup diff --git a/Algebra.Properties.Ring.html b/Algebra.Properties.Ring.html index 3e463b0..b6f643a 100644 --- a/Algebra.Properties.Ring.html +++ b/Algebra.Properties.Ring.html @@ -1,5 +1,5 @@ -Algebra.Properties.Ring Source code on Github------------------------------------------------------------------------ +Algebra.Properties.Ring Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some basic properties of Rings diff --git a/Algebra.Properties.RingWithoutOne.html b/Algebra.Properties.RingWithoutOne.html index 2a63b80..3901392 100644 --- a/Algebra.Properties.RingWithoutOne.html +++ b/Algebra.Properties.RingWithoutOne.html @@ -1,5 +1,5 @@ -Algebra.Properties.RingWithoutOne Source code on Github------------------------------------------------------------------------ +Algebra.Properties.RingWithoutOne Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some basic properties of RingWithoutOne diff --git a/Algebra.Properties.Semigroup.html b/Algebra.Properties.Semigroup.html index 7c3d12d..8d491e0 100644 --- a/Algebra.Properties.Semigroup.html +++ b/Algebra.Properties.Semigroup.html @@ -1,5 +1,5 @@ -Algebra.Properties.Semigroup Source code on Github------------------------------------------------------------------------ +Algebra.Properties.Semigroup Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some theory for Semigroup diff --git a/Algebra.Properties.Semiring.Exp.html b/Algebra.Properties.Semiring.Exp.html index e9266a7..977bb10 100644 --- a/Algebra.Properties.Semiring.Exp.html +++ b/Algebra.Properties.Semiring.Exp.html @@ -1,5 +1,5 @@ -Algebra.Properties.Semiring.Exp Source code on Github------------------------------------------------------------------------ +Algebra.Properties.Semiring.Exp Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Exponentiation defined over a semiring as repeated multiplication diff --git a/Algebra.Solver.Ring.AlmostCommutativeRing.html b/Algebra.Solver.Ring.AlmostCommutativeRing.html index c23366c..d05a3c0 100644 --- a/Algebra.Solver.Ring.AlmostCommutativeRing.html +++ b/Algebra.Solver.Ring.AlmostCommutativeRing.html @@ -1,5 +1,5 @@ -Algebra.Solver.Ring.AlmostCommutativeRing Source code on Github------------------------------------------------------------------------ +Algebra.Solver.Ring.AlmostCommutativeRing Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Commutative semirings with some additional structure ("almost" diff --git a/Algebra.Solver.Ring.Lemmas.html b/Algebra.Solver.Ring.Lemmas.html index 963a967..c303cf2 100644 --- a/Algebra.Solver.Ring.Lemmas.html +++ b/Algebra.Solver.Ring.Lemmas.html @@ -1,5 +1,5 @@ -Algebra.Solver.Ring.Lemmas Source code on Github------------------------------------------------------------------------ +Algebra.Solver.Ring.Lemmas Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some boring lemmas used by the ring solver diff --git a/Algebra.Solver.Ring.Simple.html b/Algebra.Solver.Ring.Simple.html index 34ca7b6..3827c7f 100644 --- a/Algebra.Solver.Ring.Simple.html +++ b/Algebra.Solver.Ring.Simple.html @@ -1,5 +1,5 @@ -Algebra.Solver.Ring.Simple Source code on Github------------------------------------------------------------------------ +Algebra.Solver.Ring.Simple Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Instantiates the ring solver with two copies of the same ring with diff --git a/Algebra.Solver.Ring.html b/Algebra.Solver.Ring.html index b2050bc..3cc86ac 100644 --- a/Algebra.Solver.Ring.html +++ b/Algebra.Solver.Ring.html @@ -1,5 +1,5 @@ -Algebra.Solver.Ring Source code on Github------------------------------------------------------------------------ +Algebra.Solver.Ring Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Old solver for commutative ring or semiring equalities diff --git a/Algebra.Structures.Biased.html b/Algebra.Structures.Biased.html index c67e4e7..5845dfa 100644 --- a/Algebra.Structures.Biased.html +++ b/Algebra.Structures.Biased.html @@ -1,5 +1,5 @@ -Algebra.Structures.Biased Source code on Github------------------------------------------------------------------------ +Algebra.Structures.Biased Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Ways to give instances of certain structures where some fields can diff --git a/Algebra.Structures.html b/Algebra.Structures.html index 9f17153..9397866 100644 --- a/Algebra.Structures.html +++ b/Algebra.Structures.html @@ -1,5 +1,5 @@ -Algebra.Structures Source code on Github------------------------------------------------------------------------ +Algebra.Structures Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Some algebraic structures (not packed up with sets, operations, etc.) diff --git a/Algebra.html b/Algebra.html index a5a1d86..4a8c418 100644 --- a/Algebra.html +++ b/Algebra.html @@ -1,5 +1,5 @@ -Algebra Source code on Github------------------------------------------------------------------------ +Algebra Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Definitions of algebraic structures like monoids and rings diff --git a/Axiom.Extensionality.Propositional.html b/Axiom.Extensionality.Propositional.html index 7120eda..731808a 100644 --- a/Axiom.Extensionality.Propositional.html +++ b/Axiom.Extensionality.Propositional.html @@ -1,5 +1,5 @@ -Axiom.Extensionality.Propositional Source code on Github------------------------------------------------------------------------ +Axiom.Extensionality.Propositional Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Results concerning function extensionality for propositional equality diff --git a/Axiom.UniquenessOfIdentityProofs.html b/Axiom.UniquenessOfIdentityProofs.html index a7ba911..2eb7a80 100644 --- a/Axiom.UniquenessOfIdentityProofs.html +++ b/Axiom.UniquenessOfIdentityProofs.html @@ -1,5 +1,5 @@ -Axiom.UniquenessOfIdentityProofs Source code on Github------------------------------------------------------------------------ +Axiom.UniquenessOfIdentityProofs Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Results concerning uniqueness of identity proofs diff --git a/Class.Applicative.Core.html b/Class.Applicative.Core.html index ba82dfb..0f6df0b 100644 --- a/Class.Applicative.Core.html +++ b/Class.Applicative.Core.html @@ -1,5 +1,5 @@ -Class.Applicative.Core Source code on Github{-# OPTIONS --without-K #-} +Class.Applicative.Core Source code on Github{-# OPTIONS --without-K #-} module Class.Applicative.Core where open import Class.Prelude diff --git a/Class.Applicative.Instances.html b/Class.Applicative.Instances.html index fa6839d..0d477f7 100644 --- a/Class.Applicative.Instances.html +++ b/Class.Applicative.Instances.html @@ -1,5 +1,5 @@ -Class.Applicative.Instances Source code on Github{-# OPTIONS --without-K #-} +Class.Applicative.Instances Source code on Github{-# OPTIONS --without-K #-} module Class.Applicative.Instances where open import Class.Prelude diff --git a/Class.Applicative.html b/Class.Applicative.html index 5bd126e..f095964 100644 --- a/Class.Applicative.html +++ b/Class.Applicative.html @@ -1,5 +1,5 @@ -Class.Applicative Source code on Github{-# OPTIONS --without-K #-} +Class.Applicative Source code on Github{-# OPTIONS --without-K #-} module Class.Applicative where open import Class.Applicative.Core public diff --git a/Class.Core.html b/Class.Core.html index a846c53..8bc9392 100644 --- a/Class.Core.html +++ b/Class.Core.html @@ -1,5 +1,5 @@ -Class.Core Source code on Github{-# OPTIONS --without-K #-} +Class.Core Source code on Github{-# OPTIONS --without-K #-} module Class.Core where open import Class.Prelude diff --git a/Class.DecEq.Core.html b/Class.DecEq.Core.html index e03f9dc..a98e880 100644 --- a/Class.DecEq.Core.html +++ b/Class.DecEq.Core.html @@ -1,5 +1,5 @@ -Class.DecEq.Core Source code on Github{-# OPTIONS --without-K #-} +Class.DecEq.Core Source code on Github{-# OPTIONS --without-K #-} module Class.DecEq.Core where open import Class.Prelude diff --git a/Class.DecEq.Instances.html b/Class.DecEq.Instances.html index d3901f5..6f37260 100644 --- a/Class.DecEq.Instances.html +++ b/Class.DecEq.Instances.html @@ -1,5 +1,5 @@ -Class.DecEq.Instances Source code on Github{-# OPTIONS --without-K #-} +Class.DecEq.Instances Source code on Github{-# OPTIONS --without-K #-} module Class.DecEq.Instances where open import Class.Prelude diff --git a/Class.DecEq.html b/Class.DecEq.html index c7aacce..9de63e7 100644 --- a/Class.DecEq.html +++ b/Class.DecEq.html @@ -1,5 +1,5 @@ -Class.DecEq Source code on Github{-# OPTIONS --without-K #-} +Class.DecEq Source code on Github{-# OPTIONS --without-K #-} module Class.DecEq where open import Class.DecEq.Core public diff --git a/Class.Functor.Core.html b/Class.Functor.Core.html index 5a697e8..969480e 100644 --- a/Class.Functor.Core.html +++ b/Class.Functor.Core.html @@ -1,5 +1,5 @@ -Class.Functor.Core Source code on Github{-# OPTIONS --without-K #-} +Class.Functor.Core Source code on Github{-# OPTIONS --without-K #-} module Class.Functor.Core where open import Class.Prelude diff --git a/Class.Functor.Instances.html b/Class.Functor.Instances.html index 51a3b27..769949b 100644 --- a/Class.Functor.Instances.html +++ b/Class.Functor.Instances.html @@ -1,5 +1,5 @@ -Class.Functor.Instances Source code on Github{-# OPTIONS --without-K #-} +Class.Functor.Instances Source code on Github{-# OPTIONS --without-K #-} module Class.Functor.Instances where open import Class.Prelude diff --git a/Class.Functor.html b/Class.Functor.html index 535d9de..6cf425d 100644 --- a/Class.Functor.html +++ b/Class.Functor.html @@ -1,5 +1,5 @@ -Class.Functor Source code on Github{-# OPTIONS --without-K #-} +Class.Functor Source code on Github{-# OPTIONS --without-K #-} module Class.Functor where open import Class.Functor.Core public diff --git a/Class.Monad.Core.html b/Class.Monad.Core.html index a3a105f..cc1dea7 100644 --- a/Class.Monad.Core.html +++ b/Class.Monad.Core.html @@ -1,5 +1,5 @@ -Class.Monad.Core Source code on Github{-# OPTIONS --without-K #-} +Class.Monad.Core Source code on Github{-# OPTIONS --without-K #-} module Class.Monad.Core where open import Class.Prelude diff --git a/Class.Monad.Instances.html b/Class.Monad.Instances.html index 6f041f0..904617a 100644 --- a/Class.Monad.Instances.html +++ b/Class.Monad.Instances.html @@ -1,5 +1,5 @@ -Class.Monad.Instances Source code on Github{-# OPTIONS --without-K #-} +Class.Monad.Instances Source code on Github{-# OPTIONS --without-K #-} module Class.Monad.Instances where open import Class.Prelude diff --git a/Class.Monad.html b/Class.Monad.html index 133474c..1d330bc 100644 --- a/Class.Monad.html +++ b/Class.Monad.html @@ -1,5 +1,5 @@ -Class.Monad Source code on Github{-# OPTIONS --without-K #-} +Class.Monad Source code on Github{-# OPTIONS --without-K #-} module Class.Monad where open import Class.Monad.Core public diff --git a/Class.MonadError.Instances.html b/Class.MonadError.Instances.html index 0037323..e886cb9 100644 --- a/Class.MonadError.Instances.html +++ b/Class.MonadError.Instances.html @@ -1,5 +1,5 @@ -Class.MonadError.Instances Source code on Github{-# OPTIONS --safe --without-K #-} +Class.MonadError.Instances Source code on Github{-# OPTIONS --safe --without-K #-} module Class.MonadError.Instances where open import Class.MonadError public diff --git a/Class.MonadError.html b/Class.MonadError.html index c17294a..d0900b5 100644 --- a/Class.MonadError.html +++ b/Class.MonadError.html @@ -1,5 +1,5 @@ -Class.MonadError Source code on Github{-# OPTIONS --safe --without-K #-} +Class.MonadError Source code on Github{-# OPTIONS --safe --without-K #-} open import Level diff --git a/Class.MonadReader.Instances.html b/Class.MonadReader.Instances.html index 493958b..1761210 100644 --- a/Class.MonadReader.Instances.html +++ b/Class.MonadReader.Instances.html @@ -1,5 +1,5 @@ -Class.MonadReader.Instances Source code on Github{-# OPTIONS --safe --without-K #-} +Class.MonadReader.Instances Source code on Github{-# OPTIONS --safe --without-K #-} module Class.MonadReader.Instances where open import Class.MonadReader public diff --git a/Class.MonadReader.html b/Class.MonadReader.html index 9e16505..d5c77dc 100644 --- a/Class.MonadReader.html +++ b/Class.MonadReader.html @@ -1,5 +1,5 @@ -Class.MonadReader Source code on Github{-# OPTIONS --safe --without-K #-} +Class.MonadReader Source code on Github{-# OPTIONS --safe --without-K #-} module Class.MonadReader where diff --git a/Class.MonadTC.Instances.html b/Class.MonadTC.Instances.html index 3bd6221..8bf8de5 100644 --- a/Class.MonadTC.Instances.html +++ b/Class.MonadTC.Instances.html @@ -1,7 +1,7 @@ -Class.MonadTC.Instances Source code on Github{-# OPTIONS --safe --without-K #-} +Class.MonadTC.Instances Source code on Github{-# OPTIONS --safe --without-K #-} module Class.MonadTC.Instances where open import Class.MonadTC public -open MonadTC ⦃...⦄ public +open MonadTC ⦃...⦄ public\ No newline at end of file diff --git a/Class.MonadTC.html b/Class.MonadTC.html index da525de..33b8b39 100644 --- a/Class.MonadTC.html +++ b/Class.MonadTC.html @@ -1,5 +1,5 @@ -Class.MonadTC Source code on Github{-# OPTIONS --safe --without-K #-} +Class.MonadTC Source code on Github{-# OPTIONS --safe --without-K #-} module Class.MonadTC where @@ -13,357 +13,428 @@ open import Reflection.Debug -open import Class.MonadReader -open import Class.MonadError -open import Class.Functor -open import Class.Monad -open import Class.Traversable - -private variable - a f : Level - A B : Set f - -data ReductionOptions : Set where - onlyReduce : List Name → ReductionOptions - dontReduce : List Name → ReductionOptions - -reduceAll : ReductionOptions -reduceAll = dontReduce [] - -record TCOptions : Set where - field - debug : DebugOptions - fuel : List (String × ℕ) - -defaultTCOptions : TCOptions -defaultTCOptions = record - { debug = defaultDebugOptions - ; fuel = [] } - -record TCEnv : Set where - field - normalisation : Bool - reconstruction : Bool - noConstraints : Bool - reduction : ReductionOptions - globalContext : Telescope - localContext : Telescope - goal : Term ⊎ Type - options : TCOptions - - open TCOptions options public - -initTCEnvWithGoal : Term → R.TC TCEnv -initTCEnvWithGoal goal = R.getContext <&> λ ctx → record - { normalisation = false - ; reconstruction = false - ; noConstraints = false - ; reduction = reduceAll - ; globalContext = ctx - ; localContext = [] - ; goal = inj₁ goal - ; options = defaultTCOptions - } - -initTCEnv : R.TC TCEnv -initTCEnv = initTCEnvWithGoal unknown - -record MonadTC (M : ∀ {f} → Set f → Set f) - ⦃ m : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ : Setω₁ where - field - unify : Term → Term → M ⊤ - typeError : ∀ {A : Set f} → List ErrorPart → M A - inferType : Term → M Type - checkType : Term → Type → M Term - normalise : Term → M Term - reduce : Term → M Term - quoteTC : A → M Term - unquoteTC : Term → M A - quoteωTC : ∀ {A : Setω} → A → M Term - freshName : String → M Name - declareDef : Arg Name → Type → M ⊤ - declarePostulate : Arg Name → Type → M ⊤ - defineFun : Name → List Clause → M ⊤ - getType : Name → M Type - getDefinition : Name → M Definition - blockOnMeta : Meta → M A - commitTC : M ⊤ - isMacro : Name → M Bool - debugPrint : String → ℕ → List ErrorPart → M ⊤ - runSpeculative : M (A × Bool) → M A - getInstances : Meta → M (List Term) - - instance _ = Functor-M {M = M} - open MonadError me - - runAndReset : M A → M A - runAndReset x = runSpeculative ((_, false) <$> x) - - -- dry-run and return true iff no error occured - -- does not change any state - isSuccessful : M A → M Bool - isSuccessful x = runAndReset (catch (x >> return true) (λ _ → return false)) - - -- TODO: return true on function, axiom and prim-fun constructors? - isDef : Name → M Bool - isDef n = do - constructor′ _ _ ← getDefinition n - where _ → return true - return false - - isCon : Name → M Bool - isCon n = do - constructor′ _ _ ← getDefinition n - where _ → return false - return true - - nameConstr : Name → List (Arg Term) → M Term - nameConstr n args = do - isD ← isDef n - isC ← isCon n - case (isD , isC) of λ where - (true , _) → return $ def n args - (false , true) → return $ con n args - (false , false) → error ((R'.primShowQName n <+> "is neither a definition nor a constructor!") ∷ᵈ []) - - termFromName : Name → M Term - termFromName n = nameConstr n [] - - -- apply the unique constructor of the record to the arguments - mkRecord : Name → List (Arg Term) → M Term - mkRecord n args = do - (record′ c _) ← getDefinition n - where _ → error ("Not a record!" ∷ᵈ []) - return $ con c args - - -- this allows mutual recursion - declareAndDefineFuns : List (Arg Name × Type × List Clause) → M ⊤ - declareAndDefineFuns ds = do - traverse (λ (n , t , _) → declareDef n t) ds - traverse (λ where (arg _ n , _ , cs) → defineFun n cs) ds - return _ - - declareAndDefineFun : Arg Name → Type → List Clause → M ⊤ - declareAndDefineFun n ty cls = declareAndDefineFuns [ (n , ty , cls) ] - - newMeta : Term → M Term - newMeta = checkType unknown - -module _ {M : ∀ {f} → Set f → Set f} - ⦃ m : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ ⦃ mtc : MonadTC M ⦄ ⦃ mre : MonadReader TCEnv M ⦄ where - - instance _ = Functor-M {M = M} - open MonadError me - open MonadTC mtc - open MonadReader mre - - record IsMErrorPart (A : Set a) : Setω where - field toMErrorPart : A → M (List ErrorPart) - - open IsMErrorPart ⦃...⦄ public - - data MErrorPartWrap : Set where - wrap : M (List ErrorPart) → MErrorPartWrap - - IsMErrorPart-IsErrorPart : ⦃ _ : IsErrorPart A ⦄ → IsMErrorPart A - IsMErrorPart-IsErrorPart .toMErrorPart a = return [ toErrorPart a ] - - instance - IsMErrorPart-String : IsMErrorPart String - IsMErrorPart-String = IsMErrorPart-IsErrorPart - - IsMErrorPart-Term : IsMErrorPart Term - IsMErrorPart-Term = IsMErrorPart-IsErrorPart - - IsMErrorPart-Name : IsMErrorPart Name - IsMErrorPart-Name = IsMErrorPart-IsErrorPart - - IsMErrorPart-MErrorPartWrap : IsMErrorPart MErrorPartWrap - IsMErrorPart-MErrorPartWrap .toMErrorPart (wrap a) = a - - []ᵐ : M (List ErrorPart) - []ᵐ = return [] - - infixr 5 _∷ᵈᵐ_ - _∷ᵈᵐ_ : A → ⦃ _ : IsMErrorPart A ⦄ → M (List ErrorPart) → M (List ErrorPart) - e ∷ᵈᵐ es = do e ← toMErrorPart e; es ← es; return (e ++ es) - - _ᵛ : A → MErrorPartWrap - a ᵛ = wrap do a ← quoteTC a; return (a ∷ᵈ []) - - _ᵛⁿ : A → MErrorPartWrap - a ᵛⁿ = wrap do a ← local (λ env → record env { normalisation = true }) $ quoteTC a; return (a ∷ᵈ []) - - _ᵗ : Term → MErrorPartWrap - t ᵗ = wrap do T ← inferType t; return (t ∷ᵈ " : " ∷ᵈ T ∷ᵈ []) - - debugLog : List ErrorPart → M ⊤ - debugLog es = do - record { options = record { debug = debug } } ← ask - if debug .DebugOptions.filter (debug .DebugOptions.path) - then debugPrint (debugOptionsPath debug) (debug .DebugOptions.level) - (debugPrintPrefix debug ∷ es) - else return tt - - debugLogᵐ : M (List ErrorPart) → M ⊤ - debugLogᵐ x = do x ← x; debugLog x - - debugLog1ᵐ : A → ⦃ _ : IsMErrorPart A ⦄ → M ⊤ - debugLog1ᵐ a = debugLogᵐ (a ∷ᵈᵐ []ᵐ) - - -- withDebugOptions : DebugOptions → M A → M A - -- withDebugOptions opts x = local (λ where - -- env@record { debug = opts' } → record env { debug = specializeDebugOptions opts' opts }) x - - withAppendDebugPath : String → M A → M A - withAppendDebugPath path x = local (λ where - env@record { options = o@record { debug = opts } } → record env { - options = record o { debug = record opts { path = opts .DebugOptions.path ∷ʳ path } } }) x - - noConstraints : M A → M A - noConstraints = local λ e → record e { noConstraints = true } - - hasType : Term → Type → M Bool - hasType t ty = isSuccessful (noConstraints $ checkType t ty) - - hasType' : Name → Type → M Bool - hasType' n ty = isSuccessful $ noConstraints $ do - t ← termFromName n - t' ← checkType t ty - if isAppliedToUnknownsAndMetas t' - then return tt - else error ("This makes the function return false" ∷ᵈ []) - where - isUnknownsAndMetas : List (Arg Term) → Bool - isUnknownsAndMetas [] = true - isUnknownsAndMetas (arg i (meta x x₁) ∷ l) = isUnknownsAndMetas l - isUnknownsAndMetas (arg i unknown ∷ l) = isUnknownsAndMetas l - isUnknownsAndMetas (arg i _ ∷ l) = false - - isAppliedToUnknownsAndMetas : Term → Bool - isAppliedToUnknownsAndMetas (var x args) = isUnknownsAndMetas args - isAppliedToUnknownsAndMetas (con c args) = isUnknownsAndMetas args - isAppliedToUnknownsAndMetas (def f args) = isUnknownsAndMetas args - isAppliedToUnknownsAndMetas (pat-lam cs args) = isUnknownsAndMetas args - isAppliedToUnknownsAndMetas (meta x args) = isUnknownsAndMetas args - isAppliedToUnknownsAndMetas _ = true - - extendContext : String × Arg Type → M A → M A - extendContext ty = local λ where e@record { localContext = Γ } → record e { localContext = ty ∷ Γ } - - getContext : M Telescope - getContext = reader λ where - e@record { localContext = Γ ; globalContext = Γ' } → Γ Data.List.++ Γ' - - getLocalContext : M Telescope - getLocalContext = reader λ where e@record { localContext = Γ } → Γ - - inContext : Telescope → M A → M A - inContext ctx = local λ e → record e { localContext = ctx } - - -- extend context by multiple variables - extendContext' : Telescope → M A → M A - extendContext' [] x = x - extendContext' (c ∷ cs) x = extendContext c (extendContext' cs x) - - dropContext : ℕ → M A → M A - dropContext n x = do - ctx ← getContext - inContext (drop n ctx) x - - logAndError : List ErrorPart → M A - logAndError e = debugLog e >> error e - - error1 : ⦃ IsErrorPart A ⦄ → A → M B - error1 a = error (a ∷ᵈ []) - - debugLog1 : ⦃ IsErrorPart A ⦄ → A → M ⊤ - debugLog1 a = debugLog (a ∷ᵈ []) - - logAndError1 : ⦃ IsErrorPart A ⦄ → A → M B - logAndError1 a = debugLog1 a >> error1 a - - markDontFail : String → M A → M A - markDontFail s x = catch x λ e → logAndError (s ∷ᵈ " should never fail! This is a bug!\nError:\n" ∷ᵈ e) - - goalTy : M Type - goalTy = do - inj₁ t ← reader TCEnv.goal - where inj₂ T → return T - inferType t - - -- take the first result if it's a just, otherwise reset the state and - -- run the second computation - runSpeculativeMaybe : M (Maybe A) → M A → M A - runSpeculativeMaybe x y = do - nothing ← runSpeculative (< id , is-just > <$> x) - where just a → return a - y - - try : List (M ⊤) → M ⊤ → M ⊤ - try [] e = e - try (x ∷ cs) e = MonadError.catch me x (λ _ → try cs e) - - getConstrs : Name → M (List (Name × Type)) - getConstrs n = do - d ← getDefinition n - cs ← case d of λ where - (record′ c fs) → return [ c ] - (data-type pars cs) → return cs - _ → error (n ∷ᵈ "is not a data or record definition!" ∷ᵈ []) - traverse (λ n → (n ,_) <$> (normalise =<< getType n)) (List Name ∋ cs) - - getConstrsForType : Term → M (List (Name × Type)) - getConstrsForType ty = do - (def n _) ← normalise ty - where _ → error (ty ∷ᵈ "does not reduce to a definition!" ∷ᵈ []) - getConstrs n - - getConstrsForTerm : Term → M (List (Name × Type)) - getConstrsForTerm t = getConstrsForType =<< inferType t - - -- run a TC computation to arrive at the term under the binder for the pattern - withPattern : Telescope → List (Arg Pattern) → M Term → M Clause - withPattern tel ps t = Clause.clause tel ps <$> extendContext' tel t - - unifyWithGoal : Term → M ⊤ - unifyWithGoal t = do - inj₁ t' ← reader TCEnv.goal - where _ → error1 "unifyWithGoal: Goal is not a term!" - unify t' t - - runWithHole : Term → M A → M A - runWithHole t = local (λ env → record env { goal = inj₁ t }) - - runWithGoalTy : Term → M A → M A - runWithGoalTy t = local (λ env → record env { goal = inj₂ t }) - - goalHole : M Term - goalHole = do - inj₂ T ← reader TCEnv.goal - where inj₁ hole → return hole - newMeta T - - withGoalHole : M ⊤ → M Term - withGoalHole tac = do - hole ← goalHole - runWithHole hole tac - return hole - - -- Finding all instance candidates of a given type. - findInstances : Type → M (List Term) - findInstances ty = runAndReset $ do - just m ← findMeta <$> newMeta ty - where _ → error1 "[findInstances] newMeta did not produce meta-variable!" - getInstances m - where - open import Data.Maybe using (_<∣>_) - findMeta = λ where - (pi (arg _ ty) (abs _ t)) → findMeta ty <∣> findMeta t - (lam _ (abs _ t)) → findMeta t - (meta m _) → just m - _ → nothing - -MonadTC-TC : MonadTC R.TC ⦃ Monad-TC ⦄ ⦃ MonadError-TC ⦄ -MonadTC-TC = record { R; R' using (quoteωTC; withReconstructed; onlyReduceDefs; dontReduceDefs; getInstances) } +open import Class.Show +open import Class.DecEq +open import Class.MonadReader +open import Class.MonadError +open import Class.Functor +open import Class.Monad +open import Class.Traversable + +private variable + a f : Level + A B : Set f + +data ReductionOptions : Set where + onlyReduce : List Name → ReductionOptions + dontReduce : List Name → ReductionOptions + +reduceAll : ReductionOptions +reduceAll = dontReduce [] + +record TCOptions : Set where + field + debug : DebugOptions + fuel : List (String × ℕ) + +defaultTCOptions : TCOptions +defaultTCOptions = record + { debug = defaultDebugOptions + ; fuel = [] } + +record TCEnv : Set where + field + normalisation : Bool + reconstruction : Bool + noConstraints : Bool + reduction : ReductionOptions + globalContext : Telescope + localContext : Telescope + goal : Term ⊎ Type + options : TCOptions + + open TCOptions options public + +initTCEnvWithGoal : Term → R.TC TCEnv +initTCEnvWithGoal goal = R.getContext <&> λ ctx → record + { normalisation = false + ; reconstruction = false + ; noConstraints = false + ; reduction = reduceAll + ; globalContext = ctx + ; localContext = [] + ; goal = inj₁ goal + ; options = defaultTCOptions + } + +initTCEnv : R.TC TCEnv +initTCEnv = initTCEnvWithGoal unknown + +record MonadTC (M : ∀ {f} → Set f → Set f) + ⦃ m : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ : Setω₁ where + field + unify : Term → Term → M ⊤ + typeError : ∀ {A : Set f} → List ErrorPart → M A + inferType : Term → M Type + checkType : Term → Type → M Term + normalise : Term → M Term + reduce : Term → M Term + quoteTC : A → M Term + unquoteTC : Term → M A + quoteωTC : ∀ {A : Setω} → A → M Term + freshName : String → M Name + declareDef : Arg Name → Type → M ⊤ + declarePostulate : Arg Name → Type → M ⊤ + defineFun : Name → List Clause → M ⊤ + getType : Name → M Type + getDefinition : Name → M Definition + blockOnMeta : Meta → M A + commitTC : M ⊤ + isMacro : Name → M Bool + debugPrint : String → ℕ → List ErrorPart → M ⊤ + runSpeculative : M (A × Bool) → M A + getInstances : Meta → M (List Term) + + instance _ = Functor-M {M = M} + open MonadError me + + runAndReset : M A → M A + runAndReset x = runSpeculative ((_, false) <$> x) + + -- dry-run and return true iff no error occured + -- does not change any state + isSuccessful : M A → M Bool + isSuccessful x = runAndReset (catch (x >> return true) (λ _ → return false)) + + -- TODO: return true on function, axiom and prim-fun constructors? + isDef : Name → M Bool + isDef n = do + constructor′ _ _ ← getDefinition n + where _ → return true + return false + + isCon : Name → M Bool + isCon n = do + constructor′ _ _ ← getDefinition n + where _ → return false + return true + + nameConstr : Name → List (Arg Term) → M Term + nameConstr n args = do + isD ← isDef n + isC ← isCon n + case (isD , isC) of λ where + (true , _) → return $ def n args + (false , true) → return $ con n args + (false , false) → error ((R'.primShowQName n <+> "is neither a definition nor a constructor!") ∷ᵈ []) + + termFromName : Name → M Term + termFromName n = nameConstr n [] + + -- apply the unique constructor of the record to the arguments + mkRecord : Name → List (Arg Term) → M Term + mkRecord n args = do + (record′ c _) ← getDefinition n + where _ → error ("Not a record!" ∷ᵈ []) + return $ con c args + + isSolvedMeta : Term → M Bool + isSolvedMeta m@(meta x args) = do + r@(meta y _) ← reduce m + where _ → return true + return (x ≠ y) + isSolvedMeta _ = error ("Not a meta!" ∷ᵈ []) + + hasUnsolvedMetas : Term → M Bool + hasUnsolvedMetas' : List (Arg Term) → M Bool + hasUnsolvedMetasCl : List Clause → M Bool + hasUnsolvedMetasTel : Telescope → M Bool + + hasUnsolvedMetas (var x args) = hasUnsolvedMetas' args + hasUnsolvedMetas (con c args) = hasUnsolvedMetas' args + hasUnsolvedMetas (def f args) = hasUnsolvedMetas' args + hasUnsolvedMetas (lam v (abs _ t)) = hasUnsolvedMetas t + hasUnsolvedMetas (pat-lam cs args) = do + a ← hasUnsolvedMetasCl cs + b ← hasUnsolvedMetas' args + return (a ∨ b) + hasUnsolvedMetas (pi (arg _ a) (abs _ b)) = do + a ← hasUnsolvedMetas a + b ← hasUnsolvedMetas b + return (a ∨ b) + hasUnsolvedMetas (sort (set t)) = hasUnsolvedMetas t + hasUnsolvedMetas (sort (prop t)) = hasUnsolvedMetas t + hasUnsolvedMetas (sort unknown) = return true + hasUnsolvedMetas (sort _) = return false + hasUnsolvedMetas (lit l) = return false + hasUnsolvedMetas m@(meta x x₁) = not <$> isSolvedMeta m + hasUnsolvedMetas unknown = return false + + hasUnsolvedMetas' [] = return false + hasUnsolvedMetas' ((arg _ x) ∷ l) = do + a ← hasUnsolvedMetas x + b ← hasUnsolvedMetas' l + return (a ∨ b) + + hasUnsolvedMetasCl [] = return false + hasUnsolvedMetasCl (clause tel _ t ∷ cl) = do + a ← hasUnsolvedMetas t + b ← hasUnsolvedMetasTel tel + c ← hasUnsolvedMetasCl cl + return (a ∨ b ∨ c) + hasUnsolvedMetasCl (absurd-clause tel _ ∷ cl) = do + a ← hasUnsolvedMetasTel tel + b ← hasUnsolvedMetasCl cl + return (a ∨ b) + + hasUnsolvedMetasTel [] = return false + hasUnsolvedMetasTel ((_ , arg _ x) ∷ tel) = do + a ← hasUnsolvedMetas x + b ← hasUnsolvedMetasTel tel + return (a ∨ b) + + -- this allows mutual recursion + declareAndDefineFuns : List (Arg Name × Type × List Clause) → M ⊤ + declareAndDefineFuns ds = do + traverse (λ (n , t , _) → declareDef n t) ds + traverse (λ where (arg _ n , _ , cs) → defineFun n cs) ds + return _ + + declareAndDefineFunsDebug : List (Arg Name × Type × List Clause) → M ⊤ + declareAndDefineFunsDebug ds = do + traverse (λ (n , t , _) → declareDef n t) ds + traverse (λ where (arg _ n , _ , _) → do + b ← getType n >>= hasUnsolvedMetas + if b then error [ strErr $ show n ] else return tt) ds + traverse (λ where (arg _ n , _ , cs) → defineFun n cs) ds + traverse (λ where (arg _ n , _ , _) → do + d@(function cs) ← getDefinition n + where _ → error [ strErr "Weird bug" ] + b ← hasUnsolvedMetasCl cs + if b then error [ strErr $ show d ] else return tt) ds + return _ + + declareAndDefineFun : Arg Name → Type → List Clause → M ⊤ + declareAndDefineFun n ty cls = declareAndDefineFuns [ (n , ty , cls) ] + + newMeta : Term → M Term + newMeta = checkType unknown + +module _ {M : ∀ {f} → Set f → Set f} + ⦃ m : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ ⦃ mtc : MonadTC M ⦄ ⦃ mre : MonadReader TCEnv M ⦄ where + + instance _ = Functor-M {M = M} + open MonadError me + open MonadTC mtc + open MonadReader mre + + record IsMErrorPart (A : Set a) : Setω where + field toMErrorPart : A → M (List ErrorPart) + + open IsMErrorPart ⦃...⦄ public + + data MErrorPartWrap : Set where + wrap : M (List ErrorPart) → MErrorPartWrap + + IsMErrorPart-IsErrorPart : ⦃ _ : IsErrorPart A ⦄ → IsMErrorPart A + IsMErrorPart-IsErrorPart .toMErrorPart a = return [ toErrorPart a ] + + instance + IsMErrorPart-String : IsMErrorPart String + IsMErrorPart-String = IsMErrorPart-IsErrorPart + + IsMErrorPart-Term : IsMErrorPart Term + IsMErrorPart-Term = IsMErrorPart-IsErrorPart + + IsMErrorPart-Name : IsMErrorPart Name + IsMErrorPart-Name = IsMErrorPart-IsErrorPart + + IsMErrorPart-MErrorPartWrap : IsMErrorPart MErrorPartWrap + IsMErrorPart-MErrorPartWrap .toMErrorPart (wrap a) = a + + []ᵐ : M (List ErrorPart) + []ᵐ = return [] + + infixr 5 _∷ᵈᵐ_ + _∷ᵈᵐ_ : A → ⦃ _ : IsMErrorPart A ⦄ → M (List ErrorPart) → M (List ErrorPart) + e ∷ᵈᵐ es = do e ← toMErrorPart e; es ← es; return (e ++ es) + + _ᵛ : A → MErrorPartWrap + a ᵛ = wrap do a ← quoteTC a; return (a ∷ᵈ []) + + _ᵛⁿ : A → MErrorPartWrap + a ᵛⁿ = wrap do a ← local (λ env → record env { normalisation = true }) $ quoteTC a; return (a ∷ᵈ []) + + _ᵗ : Term → MErrorPartWrap + t ᵗ = wrap do T ← inferType t; return (t ∷ᵈ " : " ∷ᵈ T ∷ᵈ []) + + debugLog : List ErrorPart → M ⊤ + debugLog es = do + record { options = record { debug = debug } } ← ask + if debug .DebugOptions.filter (debug .DebugOptions.path) + then debugPrint (debugOptionsPath debug) (debug .DebugOptions.level) + (debugPrintPrefix debug ∷ es) + else return tt + + debugLogᵐ : M (List ErrorPart) → M ⊤ + debugLogᵐ x = do x ← x; debugLog x + + debugLog1ᵐ : A → ⦃ _ : IsMErrorPart A ⦄ → M ⊤ + debugLog1ᵐ a = debugLogᵐ (a ∷ᵈᵐ []ᵐ) + + -- withDebugOptions : DebugOptions → M A → M A + -- withDebugOptions opts x = local (λ where + -- env@record { debug = opts' } → record env { debug = specializeDebugOptions opts' opts }) x + + withAppendDebugPath : String → M A → M A + withAppendDebugPath path x = local (λ where + env@record { options = o@record { debug = opts } } → record env { + options = record o { debug = record opts { path = opts .DebugOptions.path ∷ʳ path } } }) x + + noConstraints : M A → M A + noConstraints = local λ e → record e { noConstraints = true } + + hasType : Term → Type → M Bool + hasType t ty = isSuccessful (noConstraints $ checkType t ty) + + hasType' : Name → Type → M Bool + hasType' n ty = isSuccessful $ noConstraints $ do + t ← termFromName n + t' ← checkType t ty + if isAppliedToUnknownsAndMetas t' + then return tt + else error ("This makes the function return false" ∷ᵈ []) + where + isUnknownsAndMetas : List (Arg Term) → Bool + isUnknownsAndMetas [] = true + isUnknownsAndMetas (arg i (meta x x₁) ∷ l) = isUnknownsAndMetas l + isUnknownsAndMetas (arg i unknown ∷ l) = isUnknownsAndMetas l + isUnknownsAndMetas (arg i _ ∷ l) = false + + isAppliedToUnknownsAndMetas : Term → Bool + isAppliedToUnknownsAndMetas (var x args) = isUnknownsAndMetas args + isAppliedToUnknownsAndMetas (con c args) = isUnknownsAndMetas args + isAppliedToUnknownsAndMetas (def f args) = isUnknownsAndMetas args + isAppliedToUnknownsAndMetas (pat-lam cs args) = isUnknownsAndMetas args + isAppliedToUnknownsAndMetas (meta x args) = isUnknownsAndMetas args + isAppliedToUnknownsAndMetas _ = true + + extendContext : String × Arg Type → M A → M A + extendContext ty = local λ where e@record { localContext = Γ } → record e { localContext = ty ∷ Γ } + + getContext : M Telescope + getContext = reader λ where + e@record { localContext = Γ ; globalContext = Γ' } → Γ Data.List.++ Γ' + + getLocalContext : M Telescope + getLocalContext = reader λ where e@record { localContext = Γ } → Γ + + inContext : Telescope → M A → M A + inContext ctx = local λ e → record e { localContext = ctx } + + -- extend context by multiple variables + extendContext' : Telescope → M A → M A + extendContext' [] x = x + extendContext' (c ∷ cs) x = extendContext c (extendContext' cs x) + + dropContext : ℕ → M A → M A + dropContext n x = do + ctx ← getContext + inContext (drop n ctx) x + + logAndError : List ErrorPart → M A + logAndError e = debugLog e >> error e + + error1 : ⦃ IsErrorPart A ⦄ → A → M B + error1 a = error (a ∷ᵈ []) + + debugLog1 : ⦃ IsErrorPart A ⦄ → A → M ⊤ + debugLog1 a = debugLog (a ∷ᵈ []) + + logAndError1 : ⦃ IsErrorPart A ⦄ → A → M B + logAndError1 a = debugLog1 a >> error1 a + + markDontFail : String → M A → M A + markDontFail s x = catch x λ e → logAndError (s ∷ᵈ " should never fail! This is a bug!\nError:\n" ∷ᵈ e) + + goalTy : M Type + goalTy = do + inj₁ t ← reader TCEnv.goal + where inj₂ T → return T + inferType t + + -- take the first result if it's a just, otherwise reset the state and + -- run the second computation + runSpeculativeMaybe : M (Maybe A) → M A → M A + runSpeculativeMaybe x y = do + nothing ← runSpeculative (< id , is-just > <$> x) + where just a → return a + y + + try : List (M ⊤) → M ⊤ → M ⊤ + try [] e = e + try (x ∷ cs) e = MonadError.catch me x (λ _ → try cs e) + + getConstrs : Name → M (List (Name × Type)) + getConstrs n = do + d ← getDefinition n + cs ← case d of λ where + (record′ c fs) → return [ c ] + (data-type pars cs) → return cs + _ → error (n ∷ᵈ "is not a data or record definition!" ∷ᵈ []) + traverse (λ n → (n ,_) <$> (normalise =<< getType n)) (List Name ∋ cs) + + getConstrsForType : Term → M (List (Name × Type)) + getConstrsForType ty = do + (def n _) ← normalise ty + where _ → error (ty ∷ᵈ "does not reduce to a definition!" ∷ᵈ []) + getConstrs n + + getConstrsForTerm : Term → M (List (Name × Type)) + getConstrsForTerm t = getConstrsForType =<< inferType t + + -- run a TC computation to arrive at the term under the binder for the pattern + withPattern : Telescope → List (Arg Pattern) → M Term → M Clause + withPattern tel ps t = Clause.clause tel ps <$> extendContext' tel t + + unifyWithGoal : Term → M ⊤ + unifyWithGoal t = do + inj₁ t' ← reader TCEnv.goal + where _ → error1 "unifyWithGoal: Goal is not a term!" + unify t' t + + runWithHole : Term → M A → M A + runWithHole t = local (λ env → record env { goal = inj₁ t }) + + runWithGoalTy : Term → M A → M A + runWithGoalTy t = local (λ env → record env { goal = inj₂ t }) + + goalHole : M Term + goalHole = do + inj₂ T ← reader TCEnv.goal + where inj₁ hole → return hole + newMeta T + + withGoalHole : M ⊤ → M Term + withGoalHole tac = do + hole ← goalHole + runWithHole hole tac + return hole + + -- Finding all instance candidates of a given type. + findInstances : Type → M (List Term) + findInstances ty = runAndReset $ do + just m ← findMeta <$> newMeta ty + where _ → error1 "[findInstances] newMeta did not produce meta-variable!" + getInstances m + where + open import Data.Maybe using (_<∣>_) + findMeta = λ where + (pi (arg _ ty) (abs _ t)) → findMeta ty <∣> findMeta t + (lam _ (abs _ t)) → findMeta t + (meta m _) → just m + _ → nothing + +MonadTC-TC : MonadTC R.TC ⦃ Monad-TC ⦄ ⦃ MonadError-TC ⦄ +MonadTC-TC = record { R; R' using (quoteωTC; withReconstructed; onlyReduceDefs; dontReduceDefs; getInstances) }\ No newline at end of file diff --git a/Class.Prelude.html b/Class.Prelude.html index 2c43953..71d47f6 100644 --- a/Class.Prelude.html +++ b/Class.Prelude.html @@ -1,5 +1,5 @@ -Class.Prelude Source code on Github{-# OPTIONS --without-K #-} +Class.Prelude Source code on Github{-# OPTIONS --without-K #-} module Class.Prelude where open import Agda.Primitive public diff --git a/Class.Semigroup.Core.html b/Class.Semigroup.Core.html index 6dac670..7bf090f 100644 --- a/Class.Semigroup.Core.html +++ b/Class.Semigroup.Core.html @@ -1,5 +1,5 @@ -Class.Semigroup.Core Source code on Github{-# OPTIONS --without-K #-} +Class.Semigroup.Core Source code on Github{-# OPTIONS --without-K #-} module Class.Semigroup.Core where open import Class.Prelude diff --git a/Class.Semigroup.Instances.html b/Class.Semigroup.Instances.html index 0350df2..5d6eeb3 100644 --- a/Class.Semigroup.Instances.html +++ b/Class.Semigroup.Instances.html @@ -1,5 +1,5 @@ -Class.Semigroup.Instances Source code on Github{-# OPTIONS --without-K #-} +Class.Semigroup.Instances Source code on Github{-# OPTIONS --without-K #-} module Class.Semigroup.Instances where open import Class.Prelude diff --git a/Class.Semigroup.html b/Class.Semigroup.html index 52e90ec..096bc06 100644 --- a/Class.Semigroup.html +++ b/Class.Semigroup.html @@ -1,5 +1,5 @@ -Class.Semigroup Source code on Github{-# OPTIONS --without-K #-} +Class.Semigroup Source code on Github{-# OPTIONS --without-K #-} module Class.Semigroup where open import Class.Semigroup.Core public diff --git a/Class.Show.Core.html b/Class.Show.Core.html index e2d738e..165ddcf 100644 --- a/Class.Show.Core.html +++ b/Class.Show.Core.html @@ -1,5 +1,5 @@ -Class.Show.Core Source code on Github{-# OPTIONS --without-K #-} +Class.Show.Core Source code on Github{-# OPTIONS --without-K #-} module Class.Show.Core where open import Class.Prelude diff --git a/Class.Show.Instances.html b/Class.Show.Instances.html index 4dce9c1..ad8a5d8 100644 --- a/Class.Show.Instances.html +++ b/Class.Show.Instances.html @@ -1,5 +1,5 @@ -Class.Show.Instances Source code on Github{-# OPTIONS --without-K #-} +Class.Show.Instances Source code on Github{-# OPTIONS --without-K #-} module Class.Show.Instances where open import Class.Prelude hiding (Type) diff --git a/Class.Show.html b/Class.Show.html index 1eb1e0c..70f43f8 100644 --- a/Class.Show.html +++ b/Class.Show.html @@ -1,5 +1,5 @@ -Class.Show Source code on Github{-# OPTIONS --without-K #-} +Class.Show Source code on Github{-# OPTIONS --without-K #-} module Class.Show where open import Class.Show.Core public diff --git a/Class.Traversable.Core.html b/Class.Traversable.Core.html index a1bbd4a..d19a0d4 100644 --- a/Class.Traversable.Core.html +++ b/Class.Traversable.Core.html @@ -1,5 +1,5 @@ -Class.Traversable.Core Source code on Github{-# OPTIONS --without-K #-} +Class.Traversable.Core Source code on Github{-# OPTIONS --without-K #-} module Class.Traversable.Core where open import Class.Prelude diff --git a/Class.Traversable.Instances.html b/Class.Traversable.Instances.html index 454f850..a23a936 100644 --- a/Class.Traversable.Instances.html +++ b/Class.Traversable.Instances.html @@ -1,5 +1,5 @@ -Class.Traversable.Instances Source code on Github{-# OPTIONS --without-K #-} +Class.Traversable.Instances Source code on Github{-# OPTIONS --without-K #-} module Class.Traversable.Instances where open import Class.Prelude diff --git a/Class.Traversable.html b/Class.Traversable.html index c9bec94..17d8f16 100644 --- a/Class.Traversable.html +++ b/Class.Traversable.html @@ -1,5 +1,5 @@ -Class.Traversable Source code on Github{-# OPTIONS --without-K #-} +Class.Traversable Source code on Github{-# OPTIONS --without-K #-} module Class.Traversable where open import Class.Traversable.Core public diff --git a/Data.Bool.Base.html b/Data.Bool.Base.html index 63f5a15..4973546 100644 --- a/Data.Bool.Base.html +++ b/Data.Bool.Base.html @@ -1,5 +1,5 @@ -Data.Bool.Base Source code on Github------------------------------------------------------------------------ +Data.Bool.Base Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- The type for booleans and some operations diff --git a/Data.Bool.Properties.html b/Data.Bool.Properties.html index eb5389d..8111c13 100644 --- a/Data.Bool.Properties.html +++ b/Data.Bool.Properties.html @@ -1,5 +1,5 @@ -Data.Bool.Properties Source code on Github------------------------------------------------------------------------ +Data.Bool.Properties Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- A bunch of properties diff --git a/Data.Bool.Show.html b/Data.Bool.Show.html index 998d6db..f5a9fa8 100644 --- a/Data.Bool.Show.html +++ b/Data.Bool.Show.html @@ -1,5 +1,5 @@ -Data.Bool.Show Source code on Github------------------------------------------------------------------------ +Data.Bool.Show Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Showing booleans diff --git a/Data.Bool.html b/Data.Bool.html index 46d4467..0f9f05e 100644 --- a/Data.Bool.html +++ b/Data.Bool.html @@ -1,5 +1,5 @@ -Data.Bool Source code on Github------------------------------------------------------------------------ +Data.Bool Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Booleans diff --git a/Data.Char.Base.html b/Data.Char.Base.html index 1c67ae8..333d5f2 100644 --- a/Data.Char.Base.html +++ b/Data.Char.Base.html @@ -1,5 +1,5 @@ -Data.Char.Base Source code on Github------------------------------------------------------------------------ +Data.Char.Base Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Basic definitions for Characters diff --git a/Data.Char.Properties.html b/Data.Char.Properties.html index 60c29ce..2e7ee8c 100644 --- a/Data.Char.Properties.html +++ b/Data.Char.Properties.html @@ -1,5 +1,5 @@ -Data.Char.Properties Source code on Github------------------------------------------------------------------------ +Data.Char.Properties Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of operations on characters diff --git a/Data.Char.html b/Data.Char.html index 66c8da3..e338858 100644 --- a/Data.Char.html +++ b/Data.Char.html @@ -1,5 +1,5 @@ -Data.Char Source code on Github------------------------------------------------------------------------ +Data.Char Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Characters diff --git a/Data.Container.Core.html b/Data.Container.Core.html index 3940a5e..6e6723b 100644 --- a/Data.Container.Core.html +++ b/Data.Container.Core.html @@ -1,5 +1,5 @@ -Data.Container.Core Source code on Github------------------------------------------------------------------------ +Data.Container.Core Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Containers core diff --git a/Data.Container.Membership.html b/Data.Container.Membership.html index 22e21e7..2384048 100644 --- a/Data.Container.Membership.html +++ b/Data.Container.Membership.html @@ -1,5 +1,5 @@ -Data.Container.Membership Source code on Github------------------------------------------------------------------------ +Data.Container.Membership Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Membership for containers diff --git a/Data.Container.Morphism.Properties.html b/Data.Container.Morphism.Properties.html index 0370687..91c40e6 100644 --- a/Data.Container.Morphism.Properties.html +++ b/Data.Container.Morphism.Properties.html @@ -1,5 +1,5 @@ -Data.Container.Morphism.Properties Source code on Github------------------------------------------------------------------------ +Data.Container.Morphism.Properties Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Propertiers of any for containers diff --git a/Data.Container.Morphism.html b/Data.Container.Morphism.html index b4d4c06..988ca23 100644 --- a/Data.Container.Morphism.html +++ b/Data.Container.Morphism.html @@ -1,5 +1,5 @@ -Data.Container.Morphism Source code on Github------------------------------------------------------------------------ +Data.Container.Morphism Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Container Morphisms diff --git a/Data.Container.Properties.html b/Data.Container.Properties.html index 425d650..aa32691 100644 --- a/Data.Container.Properties.html +++ b/Data.Container.Properties.html @@ -1,5 +1,5 @@ -Data.Container.Properties Source code on Github------------------------------------------------------------------------ +Data.Container.Properties Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of operations on containers diff --git a/Data.Container.Related.html b/Data.Container.Related.html index ab62a38..f183e39 100644 --- a/Data.Container.Related.html +++ b/Data.Container.Related.html @@ -1,5 +1,5 @@ -Data.Container.Related Source code on Github------------------------------------------------------------------------ +Data.Container.Related Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Several kinds of "relatedness" for containers such as equivalences, diff --git a/Data.Container.Relation.Binary.Equality.Setoid.html b/Data.Container.Relation.Binary.Equality.Setoid.html index a676f2f..631910a 100644 --- a/Data.Container.Relation.Binary.Equality.Setoid.html +++ b/Data.Container.Relation.Binary.Equality.Setoid.html @@ -1,5 +1,5 @@ -Data.Container.Relation.Binary.Equality.Setoid Source code on Github------------------------------------------------------------------------ +Data.Container.Relation.Binary.Equality.Setoid Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Equality over container extensions parametrised by some setoid diff --git a/Data.Container.Relation.Binary.Pointwise.Properties.html b/Data.Container.Relation.Binary.Pointwise.Properties.html index 19504c5..d5c57e7 100644 --- a/Data.Container.Relation.Binary.Pointwise.Properties.html +++ b/Data.Container.Relation.Binary.Pointwise.Properties.html @@ -1,5 +1,5 @@ -Data.Container.Relation.Binary.Pointwise.Properties Source code on Github------------------------------------------------------------------------ +Data.Container.Relation.Binary.Pointwise.Properties Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of pointwise equality for containers diff --git a/Data.Container.Relation.Binary.Pointwise.html b/Data.Container.Relation.Binary.Pointwise.html index b2987a7..0934754 100644 --- a/Data.Container.Relation.Binary.Pointwise.html +++ b/Data.Container.Relation.Binary.Pointwise.html @@ -1,5 +1,5 @@ -Data.Container.Relation.Binary.Pointwise Source code on Github------------------------------------------------------------------------ +Data.Container.Relation.Binary.Pointwise Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Pointwise equality for containers diff --git a/Data.Container.Relation.Unary.All.html b/Data.Container.Relation.Unary.All.html index 262278d..b73a4c7 100644 --- a/Data.Container.Relation.Unary.All.html +++ b/Data.Container.Relation.Unary.All.html @@ -1,5 +1,5 @@ -Data.Container.Relation.Unary.All Source code on Github------------------------------------------------------------------------ +Data.Container.Relation.Unary.All Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- All (□) for containers diff --git a/Data.Container.Relation.Unary.Any.html b/Data.Container.Relation.Unary.Any.html index 5d39f46..6cad2a8 100644 --- a/Data.Container.Relation.Unary.Any.html +++ b/Data.Container.Relation.Unary.Any.html @@ -1,5 +1,5 @@ -Data.Container.Relation.Unary.Any Source code on Github------------------------------------------------------------------------ +Data.Container.Relation.Unary.Any Source code on Github------------------------------------------------------------------------ -- The Agda standard library -- -- Any (◇) for containers diff --git a/Data.Container.html b/Data.Container.html index 9934ef0..b8c7c02 100644 --- a/Data.Container.html +++ b/Data.Container.html @@ -1,5 +1,5 @@ -Data.Container Source code on Github