XDS-Agda

Library

XDS-Agda

pdmosses/xds-agda

About
About
Lambda-Calculus
Lambda-Calculus
- Definitions
  Definitions
- Domains
  Domains
- Environments
  Environments
- Semantics
  Semantics
- Terms
  Terms
- Tests
  Tests
- Variables
  Variables
PCF
PCF
- Checks
  Checks
- Constants
  Constants
- Domain-Notation
  Domain-Notation
- Environments
  Environments
- Terms
  Terms
- Types
  Types
- Variables
  Variables
Scm
Scm
- Abstract-Syntax
  Abstract-Syntax
- Auxiliary-Functions
  Auxiliary-Functions
- Domain-Equations
  Domain-Equations
- Notation
  Notation
- Semantic-Functions
  Semantic-Functions
Library
Library
- Agda
  Agda
  - Builtin
    Builtin
    
    Bool
    
    Bool
    
    Char
    
    Char
    
    Equality
    
    Equality
    
    Rewrite
    
    Rewrite
    
    Int
    
    Int
    
    List
    
    List
    
    Maybe
    
    Maybe
    
    Nat
    
    Nat
    
    Sigma
    
    Sigma
    
    Strict
    
    Strict
    
    String
    
    String
    
    Unit
    
    Unit
  - Primitive
    
    Primitive
- Algebra
  Algebra
  - Bundles
    
    Bundles
    
    Raw
    
    Raw
  - Consequences
    Consequences
    
    Base
    
    Base
    
    Propositional
    
    Propositional
    
    Setoid
    
    Setoid
  - Construct
    Construct
    
    NaturalChoice
    NaturalChoice
    
    Base
    
    Base
    
    MaxOp
    
    MaxOp
    
    MinMaxOp
    
    MinMaxOp
    
    MinOp
    
    MinOp
  - Core
    
    Core
  - Definitions
    
    Definitions
    
    RawMagma
    
    RawMagma
  - Lattice
    Lattice
    
    Bundles
    
    Bundles
    
    Raw
    
    Raw
    
    Construct
    Construct
    
    NaturalChoice
    NaturalChoice
    
    MaxOp
    
    MaxOp
    
    MinMaxOp
    
    MinMaxOp
    
    MinOp
    
    MinOp
    
    Properties
    Properties
    
    BooleanAlgebra
    
    BooleanAlgebra
    
    DistributiveLattice
    
    DistributiveLattice
    
    Lattice
    
    Lattice
    
    Semilattice
    
    Semilattice
    
    Structures
    
    Structures
  - Morphism
    
    Morphism
    
    Definitions
    
    Definitions
    
    Structures
    
    Structures
  - Properties
    Properties
    
    CommutativeSemigroup
    
    CommutativeSemigroup
    
    Group
    
    Group
    
    Loop
    
    Loop
    
    Quasigroup
    
    Quasigroup
    
    Semigroup
    
    Semigroup
  - Structures
    
    Structures
    
    Biased
    
    Biased
- Axiom
  Axiom
  - UniquenessOfIdentityProofs
    
    UniquenessOfIdentityProofs
- Data
  Data
  - Bool
    
    Bool
    
    Base
    
    Base
    
    Properties
    
    Properties
  - Char
    Char
    
    Base
    
    Base
  - Empty
    
    Empty
  - Fin
    Fin
    
    Base
    
    Base
  - Integer
    Integer
    
    Base
    
    Base
  - Irrelevant
    
    Irrelevant
  - List
    List
    
    Base
    
    Base
    
    NonEmpty
    NonEmpty
    
    Base
    
    Base
    
    Relation
    Relation
    
    Binary
    Binary
    
    Lex
    Lex
    
    Core
    
    Core
    
    Pointwise
    Pointwise
    
    Base
    
    Base
  - Maybe
    Maybe
    
    Base
    
    Base
  - Nat
    
    Nat
    
    Base
    
    Base
    
    Properties
    
    Properties
  - Parity
    Parity
    
    Base
    
    Base
  - Product
    Product
    
    Base
    
    Base
  - Sign
    Sign
    
    Base
    
    Base
  - String
    String
    
    Base
    
    Base
  - Sum
    Sum
    
    Base
    
    Base
  - These
    These
    
    Base
    
    Base
  - Unit
    Unit
    
    Base
    
    Base
    
    Polymorphic
    Polymorphic
    
    Base
    
    Base
  - Vec
    Vec
    
    Base
    
    Base
- Effect
  Effect
  - Applicative
    
    Applicative
  - Choice
    
    Choice
  - Empty
    
    Empty
  - Functor
    
    Functor
  - Monad
    
    Monad
- Function
  Function
  - Base
    
    Base
  - Bundles
    
    Bundles
  - Consequences
    
    Consequences
    
    Propositional
    
    Propositional
    
    Setoid
    
    Setoid
  - Core
    
    Core
  - Definitions
    
    Definitions
  - Dependent
    Dependent
    
    Bundles
    
    Bundles
  - Indexed
    Indexed
    
    Relation
    Relation
    
    Binary
    Binary
    
    Equality
    
    Equality
  - Metric
    Metric
    
    Bundles
    
    Bundles
    
    Core
    
    Core
    
    Definitions
    
    Definitions
    
    Nat
    
    Nat
    
    Bundles
    
    Bundles
    
    Core
    
    Core
    
    Definitions
    
    Definitions
    
    Structures
    
    Structures
    
    Structures
    
    Structures
  - Strict
    
    Strict
  - Structures
    
    Structures
    
    Biased
    
    Biased
- Induction
  Induction
  - WellFounded
    
    WellFounded
- Level
  Level
- Relation
  Relation
  - Binary
    
    Binary
    
    Bundles
    
    Bundles
    
    Raw
    
    Raw
    
    Consequences
    
    Consequences
    
    Construct
    Construct
    
    Closure
    Closure
    
    Reflexive
    
    Reflexive
    
    Composition
    
    Composition
    
    Constant
    Constant
    
    Core
    
    Core
    
    Flip
    Flip
    
    EqAndOrd
    
    EqAndOrd
    
    NaturalOrder
    NaturalOrder
    
    Left
    
    Left
    
    NonStrictToStrict
    
    NonStrictToStrict
    
    Core
    
    Core
    
    Definitions
    
    Definitions
    
    Indexed
    Indexed
    
    Heterogeneous
    
    Heterogeneous
    
    Bundles
    
    Bundles
    
    Construct
    Construct
    
    Trivial
    
    Trivial
    
    Core
    
    Core
    
    Definitions
    
    Definitions
    
    Structures
    
    Structures
    
    Lattice
    
    Lattice
    
    Bundles
    
    Bundles
    
    Definitions
    
    Definitions
    
    Structures
    
    Structures
    
    Morphism
    Morphism
    
    Definitions
    
    Definitions
    
    Structures
    
    Structures
    
    Properties
    Properties
    
    Poset
    
    Poset
    
    Preorder
    
    Preorder
    
    Setoid
    
    Setoid
    
    TotalOrder
    
    TotalOrder
    
    PropositionalEquality
    
    PropositionalEquality
    
    Algebra
    
    Algebra
    
    Core
    
    Core
    
    Properties
    
    Properties
    
    Reasoning
    Reasoning
    
    Base
    Base
    
    Double
    
    Double
    
    Single
    
    Single
    
    Triple
    
    Triple
    
    Preorder
    
    Preorder
    
    Setoid
    
    Setoid
    
    Syntax
    
    Syntax
    
    Structures
    
    Structures
    
    Biased
    
    Biased
  - Nullary
    
    Nullary
    
    Decidable
    
    Decidable
    
    Core
    
    Core
    
    Negation
    
    Negation
    
    Core
    
    Core
    
    Recomputable
    
    Recomputable
    
    Reflects
    
    Reflects
  - Unary
    
    Unary
    
    PredicateTransformer
    
    PredicateTransformer
    
    Properties
    
    Properties

Library

Note

The Agda library modules imported by non-library modules are automatically included in this section.