Signatures

Modules

• MAlonzo
  Submodules

  • Code
    Submodules

    • Agda
      Submodules

      • Builtin
        Submodules

        • MAlonzo.Code.Agda.Builtin.Bool
        •  MAlonzo.Code.Agda.Builtin.Char
          Submodules

          • MAlonzo.Code.Agda.Builtin.Char.Properties
        • MAlonzo.Code.Agda.Builtin.Coinduction
        • MAlonzo.Code.Agda.Builtin.Equality
        • MAlonzo.Code.Agda.Builtin.IO
        • MAlonzo.Code.Agda.Builtin.List
        • MAlonzo.Code.Agda.Builtin.Maybe
        • MAlonzo.Code.Agda.Builtin.Nat
        • MAlonzo.Code.Agda.Builtin.Sigma
        • MAlonzo.Code.Agda.Builtin.Strict
        •  MAlonzo.Code.Agda.Builtin.String
          Submodules

          • MAlonzo.Code.Agda.Builtin.String.Properties
        • MAlonzo.Code.Agda.Builtin.Unit
      • MAlonzo.Code.Agda.Primitive
    •  MAlonzo.Code.Algebra
      Submodules

      • MAlonzo.Code.Algebra.Bundles
      • Consequences
        Submodules

        • MAlonzo.Code.Algebra.Consequences.Base
        • MAlonzo.Code.Algebra.Consequences.Propositional
        • MAlonzo.Code.Algebra.Consequences.Setoid
      • Construct
        Submodules

        • MAlonzo.Code.Algebra.Construct.LiftedChoice
        • NaturalChoice
          Submodules

          • MAlonzo.Code.Algebra.Construct.NaturalChoice.Base
          • MAlonzo.Code.Algebra.Construct.NaturalChoice.Max
          • MAlonzo.Code.Algebra.Construct.NaturalChoice.MaxOp
          • MAlonzo.Code.Algebra.Construct.NaturalChoice.Min
          • MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp
          • MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp
        • Subst
          Submodules

          • MAlonzo.Code.Algebra.Construct.Subst.Equality
      • MAlonzo.Code.Algebra.Core
      •  MAlonzo.Code.Algebra.Definitions
        Submodules

        • MAlonzo.Code.Algebra.Definitions.RawMagma
        • MAlonzo.Code.Algebra.Definitions.RawMonoid
        • MAlonzo.Code.Algebra.Definitions.RawSemiring
      •  MAlonzo.Code.Algebra.Lattice
        Submodules

        • MAlonzo.Code.Algebra.Lattice.Bundles
        • Construct
          Submodules

          • NaturalChoice
            Submodules

            • MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MaxOp
            • MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinMaxOp
            • MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp
        • Properties
          Submodules

          • MAlonzo.Code.Algebra.Lattice.Properties.BooleanAlgebra
          • MAlonzo.Code.Algebra.Lattice.Properties.DistributiveLattice
          • MAlonzo.Code.Algebra.Lattice.Properties.Lattice
          • MAlonzo.Code.Algebra.Lattice.Properties.Semilattice
        •  MAlonzo.Code.Algebra.Lattice.Structures
          Submodules

          • MAlonzo.Code.Algebra.Lattice.Structures.Biased
      •  MAlonzo.Code.Algebra.Morphism
        Submodules

        • MAlonzo.Code.Algebra.Morphism.Definitions
        • MAlonzo.Code.Algebra.Morphism.Structures
      • Properties
        Submodules

        • MAlonzo.Code.Algebra.Properties.AbelianGroup
        • MAlonzo.Code.Algebra.Properties.CommutativeSemigroup
        • MAlonzo.Code.Algebra.Properties.DistributiveLattice
        • MAlonzo.Code.Algebra.Properties.Group
        • MAlonzo.Code.Algebra.Properties.Lattice
        • Monoid
          Submodules

          • MAlonzo.Code.Algebra.Properties.Monoid.Mult
        • MAlonzo.Code.Algebra.Properties.Ring
        • MAlonzo.Code.Algebra.Properties.Semigroup
        • Semiring
          Submodules

          • MAlonzo.Code.Algebra.Properties.Semiring.Exp
      • Solver
        Submodules

        •  MAlonzo.Code.Algebra.Solver.Ring
          Submodules

          • MAlonzo.Code.Algebra.Solver.Ring.AlmostCommutativeRing
          • MAlonzo.Code.Algebra.Solver.Ring.Lemmas
          • MAlonzo.Code.Algebra.Solver.Ring.Simple
      •  MAlonzo.Code.Algebra.Structures
        Submodules

        • MAlonzo.Code.Algebra.Structures.Biased
    • Axiom
      Submodules

      • Extensionality
        Submodules

        • MAlonzo.Code.Axiom.Extensionality.Propositional
      • MAlonzo.Code.Axiom.UniquenessOfIdentityProofs
    • Category
      Submodules

      •  MAlonzo.Code.Category.Applicative
        Submodules

        • MAlonzo.Code.Category.Applicative.Indexed
      • MAlonzo.Code.Category.Comonad
      • MAlonzo.Code.Category.Functor
      •  MAlonzo.Code.Category.Monad
        Submodules

        • MAlonzo.Code.Category.Monad.Indexed
    • Codata
      Submodules

      • Musical
        Submodules

        • Colist
          Submodules

          • MAlonzo.Code.Codata.Musical.Colist.Base
        • Conat
          Submodules

          • MAlonzo.Code.Codata.Musical.Conat.Base
        • MAlonzo.Code.Codata.Musical.Costring
        • MAlonzo.Code.Codata.Musical.Notation
    • Data
      Submodules

      •  MAlonzo.Code.Data.Bool
        Submodules

        • MAlonzo.Code.Data.Bool.Base
        • MAlonzo.Code.Data.Bool.Properties
      •  MAlonzo.Code.Data.Char
        Submodules

        • MAlonzo.Code.Data.Char.Base
        • MAlonzo.Code.Data.Char.Properties
      • MAlonzo.Code.Data.Digit
      •  MAlonzo.Code.Data.Empty
        Submodules

        • MAlonzo.Code.Data.Empty.Irrelevant
        • MAlonzo.Code.Data.Empty.Polymorphic
      •  MAlonzo.Code.Data.Fin
        Submodules

        • MAlonzo.Code.Data.Fin.Base
        • MAlonzo.Code.Data.Fin.Patterns
        • MAlonzo.Code.Data.Fin.Properties
      •  MAlonzo.Code.Data.List
        Submodules

        • MAlonzo.Code.Data.List.Base
        • MAlonzo.Code.Data.List.Categorical
        •  MAlonzo.Code.Data.List.Extrema
          Submodules

          • MAlonzo.Code.Data.List.Extrema.Core
        • Membership
          Submodules

          • MAlonzo.Code.Data.List.Membership.DecPropositional
          • MAlonzo.Code.Data.List.Membership.DecSetoid
          •  MAlonzo.Code.Data.List.Membership.Propositional
            Submodules

            •  MAlonzo.Code.Data.List.Membership.Propositional.Properties
              Submodules

              • MAlonzo.Code.Data.List.Membership.Propositional.Properties.Core
          •  MAlonzo.Code.Data.List.Membership.Setoid
            Submodules

            • MAlonzo.Code.Data.List.Membership.Setoid.Properties
        •  MAlonzo.Code.Data.List.NonEmpty
          Submodules

          • MAlonzo.Code.Data.List.NonEmpty.Base
          • MAlonzo.Code.Data.List.NonEmpty.Categorical
          • MAlonzo.Code.Data.List.NonEmpty.Properties
        • MAlonzo.Code.Data.List.Properties
        • Relation
          Submodules

          • Binary
            Submodules

            • Equality
              Submodules

              • MAlonzo.Code.Data.List.Relation.Binary.Equality.Propositional
              • MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid
            •  MAlonzo.Code.Data.List.Relation.Binary.Lex
              Submodules

              • MAlonzo.Code.Data.List.Relation.Binary.Lex.Core
              • MAlonzo.Code.Data.List.Relation.Binary.Lex.Strict
            •  MAlonzo.Code.Data.List.Relation.Binary.Pointwise
              Submodules

              • MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
              • MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties
            • Sublist
              Submodules

              •  MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous
                Submodules

                • MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core
                • MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
              • MAlonzo.Code.Data.List.Relation.Binary.Sublist.Propositional
              • MAlonzo.Code.Data.List.Relation.Binary.Sublist.Setoid
            • Subset
              Submodules

              • MAlonzo.Code.Data.List.Relation.Binary.Subset.Propositional
              • MAlonzo.Code.Data.List.Relation.Binary.Subset.Setoid
          • Unary
            Submodules

            • MAlonzo.Code.Data.List.Relation.Unary.All
            •  MAlonzo.Code.Data.List.Relation.Unary.AllPairs
              Submodules

              • MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core
            •  MAlonzo.Code.Data.List.Relation.Unary.Any
              Submodules

              • MAlonzo.Code.Data.List.Relation.Unary.Any.Properties
            • Unique
              Submodules

              • MAlonzo.Code.Data.List.Relation.Unary.Unique.Setoid
      •  MAlonzo.Code.Data.Maybe
        Submodules

        • MAlonzo.Code.Data.Maybe.Base
        • MAlonzo.Code.Data.Maybe.Categorical
        • MAlonzo.Code.Data.Maybe.Properties
        • Relation
          Submodules

          • Unary
            Submodules

            • MAlonzo.Code.Data.Maybe.Relation.Unary.All
            • MAlonzo.Code.Data.Maybe.Relation.Unary.Any
      •  MAlonzo.Code.Data.Nat
        Submodules

        • MAlonzo.Code.Data.Nat.Base
        •  MAlonzo.Code.Data.Nat.DivMod
          Submodules

          • MAlonzo.Code.Data.Nat.DivMod.Core
        •  MAlonzo.Code.Data.Nat.Divisibility
          Submodules

          • MAlonzo.Code.Data.Nat.Divisibility.Core
        • MAlonzo.Code.Data.Nat.Induction
        •  MAlonzo.Code.Data.Nat.Properties
          Submodules

          • MAlonzo.Code.Data.Nat.Properties.Core
        • MAlonzo.Code.Data.Nat.Show
        • MAlonzo.Code.Data.Nat.Solver
      •  MAlonzo.Code.Data.Product
        Submodules

        • Function
          Submodules

          • Dependent
            Submodules

            • MAlonzo.Code.Data.Product.Function.Dependent.Propositional
          • NonDependent
            Submodules

            • MAlonzo.Code.Data.Product.Function.NonDependent.Propositional
            • MAlonzo.Code.Data.Product.Function.NonDependent.Setoid
        • MAlonzo.Code.Data.Product.Properties
        • Relation
          Submodules

          • Binary
            Submodules

            • Pointwise
              Submodules

              • MAlonzo.Code.Data.Product.Relation.Binary.Pointwise.NonDependent
          • Unary
            Submodules

            • MAlonzo.Code.Data.Product.Relation.Unary.All
      •  MAlonzo.Code.Data.String
        Submodules

        • MAlonzo.Code.Data.String.Base
        • MAlonzo.Code.Data.String.Properties
      •  MAlonzo.Code.Data.Sum
        Submodules

        • MAlonzo.Code.Data.Sum.Base
        • Function
          Submodules

          • MAlonzo.Code.Data.Sum.Function.Propositional
          • MAlonzo.Code.Data.Sum.Function.Setoid
        • MAlonzo.Code.Data.Sum.Properties
        • Relation
          Submodules

          • Binary
            Submodules

            • MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise
      • These
        Submodules

        • MAlonzo.Code.Data.These.Base
      •  MAlonzo.Code.Data.Unit
        Submodules

        • MAlonzo.Code.Data.Unit.Base
        •  MAlonzo.Code.Data.Unit.Polymorphic
          Submodules

          • MAlonzo.Code.Data.Unit.Polymorphic.Base
          • MAlonzo.Code.Data.Unit.Polymorphic.Properties
        • MAlonzo.Code.Data.Unit.Properties
      • Vec
        Submodules

        • MAlonzo.Code.Data.Vec.Base
        • MAlonzo.Code.Data.Vec.Functional
        • MAlonzo.Code.Data.Vec.NZ45Zary
    •  MAlonzo.Code.Function
      Submodules

      • MAlonzo.Code.Function.Base
      • MAlonzo.Code.Function.Bijection
      • MAlonzo.Code.Function.Bundles
      • MAlonzo.Code.Function.Consequences
      • Construct
        Submodules

        • MAlonzo.Code.Function.Construct.Composition
        • MAlonzo.Code.Function.Construct.Identity
        • MAlonzo.Code.Function.Construct.Symmetry
      • MAlonzo.Code.Function.Core
      •  MAlonzo.Code.Function.Definitions
        Submodules

        • MAlonzo.Code.Function.Definitions.Core1
        • MAlonzo.Code.Function.Definitions.Core2
      • MAlonzo.Code.Function.Equality
      • MAlonzo.Code.Function.Equivalence
      • MAlonzo.Code.Function.HalfAdjointEquivalence
      • Identity
        Submodules

        • MAlonzo.Code.Function.Identity.Categorical
      • MAlonzo.Code.Function.Injection
      • MAlonzo.Code.Function.Inverse
      • MAlonzo.Code.Function.LeftInverse
      • Metric
        Submodules

        • MAlonzo.Code.Function.Metric.Bundles
        • MAlonzo.Code.Function.Metric.Core
        • MAlonzo.Code.Function.Metric.Definitions
        •  MAlonzo.Code.Function.Metric.Nat
          Submodules

          • MAlonzo.Code.Function.Metric.Nat.Bundles
          • MAlonzo.Code.Function.Metric.Nat.Core
          • MAlonzo.Code.Function.Metric.Nat.Definitions
          • MAlonzo.Code.Function.Metric.Nat.Structures
        • MAlonzo.Code.Function.Metric.Structures
      • Properties
        Submodules

        • MAlonzo.Code.Function.Properties.Bijection
        • MAlonzo.Code.Function.Properties.Inverse
        • MAlonzo.Code.Function.Properties.RightInverse
        • MAlonzo.Code.Function.Properties.Surjection
      •  MAlonzo.Code.Function.Related
        Submodules

        • MAlonzo.Code.Function.Related.Propositional
        • MAlonzo.Code.Function.Related.TypeIsomorphisms
      • MAlonzo.Code.Function.Strict
      • MAlonzo.Code.Function.Structures
      • MAlonzo.Code.Function.Surjection
    •  MAlonzo.Code.IO
      Submodules

      • MAlonzo.Code.IO.Base
      • MAlonzo.Code.IO.Finite
      • MAlonzo.Code.IO.Infinite
      •  MAlonzo.Code.IO.Primitive
        Submodules

        • MAlonzo.Code.IO.Primitive.Finite
        • MAlonzo.Code.IO.Primitive.Infinite
    •  MAlonzo.Code.Induction
      Submodules

      • MAlonzo.Code.Induction.WellFounded
    • MAlonzo.Code.Level
    • MAlonzo.Code.Lib
    • MAlonzo.Code.LibNonEmpty
    • Mint
      Submodules

      •  MAlonzo.Code.Mint.Completeness
        Submodules

        • MAlonzo.Code.Mint.Completeness.Box
        • MAlonzo.Code.Mint.Completeness.Contexts
        • MAlonzo.Code.Mint.Completeness.Fundamental
        • MAlonzo.Code.Mint.Completeness.LogRel
        • MAlonzo.Code.Mint.Completeness.Nat
        • MAlonzo.Code.Mint.Completeness.Pi
        • MAlonzo.Code.Mint.Completeness.Substitutions
        • MAlonzo.Code.Mint.Completeness.Terms
        • MAlonzo.Code.Mint.Completeness.Universe
      • MAlonzo.Code.Mint.Example
      • Semantics
        Submodules

        • MAlonzo.Code.Mint.Semantics.Domain
        • MAlonzo.Code.Mint.Semantics.Evaluation
        • MAlonzo.Code.Mint.Semantics.PER
        • Properties
          Submodules

          • MAlonzo.Code.Mint.Semantics.Properties.Domain
          • MAlonzo.Code.Mint.Semantics.Properties.Evaluation
          • NoFunExt
            Submodules

            • MAlonzo.Code.Mint.Semantics.Properties.NoFunExt.Domain
            • MAlonzo.Code.Mint.Semantics.Properties.NoFunExt.Evaluation
          •  MAlonzo.Code.Mint.Semantics.Properties.PER
            Submodules

            • MAlonzo.Code.Mint.Semantics.Properties.PER.Core
        • MAlonzo.Code.Mint.Semantics.Readback
        • MAlonzo.Code.Mint.Semantics.Realizability
      •  MAlonzo.Code.Mint.Statics
        Submodules

        • MAlonzo.Code.Mint.Statics.Concise
        • MAlonzo.Code.Mint.Statics.CtxEquiv
        • MAlonzo.Code.Mint.Statics.Equiv
        • MAlonzo.Code.Mint.Statics.Full
        • MAlonzo.Code.Mint.Statics.Misc
        • MAlonzo.Code.Mint.Statics.PER
        • MAlonzo.Code.Mint.Statics.Presup
        •  MAlonzo.Code.Mint.Statics.Properties
          Submodules

          • MAlonzo.Code.Mint.Statics.Properties.Box
          • MAlonzo.Code.Mint.Statics.Properties.Contexts
          • MAlonzo.Code.Mint.Statics.Properties.Ops
          • MAlonzo.Code.Mint.Statics.Properties.Pi
          • MAlonzo.Code.Mint.Statics.Properties.Substs
        • MAlonzo.Code.Mint.Statics.Refl
        • MAlonzo.Code.Mint.Statics.Syntax
    • Relation
      Submodules

      •  MAlonzo.Code.Relation.Binary
        Submodules

        • MAlonzo.Code.Relation.Binary.Bundles
        • MAlonzo.Code.Relation.Binary.Consequences
        • Construct
          Submodules

          • Closure
            Submodules

            •  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive
              Submodules

              • MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.Properties
          • Constant
            Submodules

            • MAlonzo.Code.Relation.Binary.Construct.Constant.Core
          • MAlonzo.Code.Relation.Binary.Construct.Converse
          • MAlonzo.Code.Relation.Binary.Construct.Intersection
          • NaturalOrder
            Submodules

            • MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left
          • MAlonzo.Code.Relation.Binary.Construct.NonStrictToStrict
          • MAlonzo.Code.Relation.Binary.Construct.On
          • Subst
            Submodules

            • MAlonzo.Code.Relation.Binary.Construct.Subst.Equality
        • MAlonzo.Code.Relation.Binary.Core
        • MAlonzo.Code.Relation.Binary.Definitions
        • Indexed
          Submodules

          •  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous
            Submodules

            • MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles
            • Construct
              Submodules

              • MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
            • MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Core
            • MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Definitions
            • MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures
        •  MAlonzo.Code.Relation.Binary.Lattice
          Submodules

          • MAlonzo.Code.Relation.Binary.Lattice.Bundles
          • MAlonzo.Code.Relation.Binary.Lattice.Definitions
          • MAlonzo.Code.Relation.Binary.Lattice.Structures
        • Morphism
          Submodules

          • MAlonzo.Code.Relation.Binary.Morphism.Definitions
          • MAlonzo.Code.Relation.Binary.Morphism.Structures
        • Properties
          Submodules

          • MAlonzo.Code.Relation.Binary.Properties.DecTotalOrder
          • MAlonzo.Code.Relation.Binary.Properties.Poset
          • MAlonzo.Code.Relation.Binary.Properties.Preorder
          • MAlonzo.Code.Relation.Binary.Properties.Setoid
          • MAlonzo.Code.Relation.Binary.Properties.TotalOrder
        •  MAlonzo.Code.Relation.Binary.PropositionalEquality
          Submodules

          • MAlonzo.Code.Relation.Binary.PropositionalEquality.Algebra
          • MAlonzo.Code.Relation.Binary.PropositionalEquality.Core
          • MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
        • Reasoning
          Submodules

          • Base
            Submodules

            • MAlonzo.Code.Relation.Binary.Reasoning.Base.Double
            • MAlonzo.Code.Relation.Binary.Reasoning.Base.Partial
            • MAlonzo.Code.Relation.Binary.Reasoning.Base.Single
            • MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple
          • MAlonzo.Code.Relation.Binary.Reasoning.PartialSetoid
          • MAlonzo.Code.Relation.Binary.Reasoning.Preorder
          • MAlonzo.Code.Relation.Binary.Reasoning.Setoid
        • MAlonzo.Code.Relation.Binary.Reflection
        • MAlonzo.Code.Relation.Binary.Structures
      •  MAlonzo.Code.Relation.Nullary
        Submodules

        •  MAlonzo.Code.Relation.Nullary.Decidable
          Submodules

          • MAlonzo.Code.Relation.Nullary.Decidable.Core
        • MAlonzo.Code.Relation.Nullary.Indexed
        •  MAlonzo.Code.Relation.Nullary.Negation
          Submodules

          • MAlonzo.Code.Relation.Nullary.Negation.Core
        • MAlonzo.Code.Relation.Nullary.Product
        • MAlonzo.Code.Relation.Nullary.Reflects
        • MAlonzo.Code.Relation.Nullary.Sum
      •  MAlonzo.Code.Relation.Unary
        Submodules

        • MAlonzo.Code.Relation.Unary.Properties
  •  MAlonzo.RTE
    Submodules

    • MAlonzo.RTE.Float