HarrisonGrodin

Standard ML Style Guide

Core Language

atexp

Special Constant: <scon>

<scon>

HarrisonGrodin

signature OBJECT =
  sig
    type 'a tag
    type t

    val new : unit -> t list tag
    and make : 'a tag -> 'a -> t
    val get : t -> 'a tag -> 'a

    (* primitives *)

HarrisonGrodin

signature OBJECT =
  sig
    type 'a tag
    type t

    val Bool : bool tag
    and Int : int tag
    and String : string tag

    val toString : t -> string

HarrisonGrodin

{-# OPTIONS --cubical #-}

open import Cubical.Foundations.Prelude

infix  1 begin_
begin_ : {A : Set} {x y : A} → x ≡ y → x ≡ y
begin_ x≡y = x≡y

infix  9 _⁻¹
infixl 5 _·_

HarrisonGrodin

signature UNIV_MAP =
  sig
    structure Key : sig
      type 'a t
      val create : unit -> 'a t
    end

    type t

    val empty : t