Denotational Semantics in Agda
ULC.Domains
Initializing search
    pdmosses/xds-agda
    • About
    • Meta-notation
    • ULC
    • PCF
    • Scheme
    pdmosses/xds-agda
    • About
    • Meta-notation
      • Untyped λ-calculus
      • ULC.All
      • ULC.Variables
      • ULC.Terms
      • ULC.Domains
      • ULC.Environments
      • ULC.Semantics
      • ULC.Checks
      • PCF (Plotkin 1977)
      • PCF.All
      • PCF.Domain Notation
      • PCF.Types
      • PCF.Constants
      • PCF.Variables
      • PCF.Terms
      • PCF.Environments
      • PCF.Checks
      • Core Scheme (R5RS)
      • Scheme.All
      • Scheme.Domain Notation
      • Scheme.Abstract Syntax
      • Scheme.Domain Equations
      • Scheme.Auxiliary Functions
      • Scheme.Semantic Functions

    ULC.Domains

    module ULC.Domains where
    
    open import Function
      using (Inverse; _↔_) public
    open Inverse {{ ... }}
      using (to; from) public
    
    postulate
      D∞ : Set
    postulate
      instance iso : D∞ ↔ (D∞ → D∞)
    
    variable d : D∞
    
    Made with Material for MkDocs