andrejbauer

{-
  Weak excluded middle states that for every propostiion P, either ¬¬P or ¬P holds.

  We give a proof of weak excluded middle, relying just on basic facts about real numbers,
  which we carefully state, in order to make the dependence on them transparent.

  Some people might doubt the formalization. To convince yourself that there is no cheating, you should:

  * Carefully read the facts listed in the RealFacts below to see that these are all
    just familiar facts about the real numbers.

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

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

    type t

    val empty : t

MohamedAlaa

tmux shortcuts & cheatsheet

start new:

tmux

start new with session name:

tmux new -s myname