ratmice

type 'a sealer_unsealer = {seal:'a -> exn, unseal:exn -> 'a option};

fun 'a mkSealer () : 'a sealer_unsealer
  = let
      (* 1:  Dynamically sealed
             It's worth noting that while this provides sealing,
             it does not provide identity or branding.

	     What makes it interesting is that it provides freshness guarantees of the exception constructor.
             exports it's constructor as a function, (rather than as a constructor).

ratmice

-- you can add extra negations if you want
def extra_negations {A : Prop} (a : A) : ¬¬A :=
  show ¬¬A, from not.intro (λ (na: ¬A), na a)
  
-- You can remove extra negations beyond 2,
def triple_elim {A : Prop} (nnna : ¬¬¬A)  : ¬A :=
  show ¬A, from not.intro (λ a, nnna (extra_negations a))

-- LEM is not negated,

ratmice

functor Fresh()
:> sig
  type t;
  
  val v : t;
end
= struct 
  type t = unit; 

  val v = {};

ratmice

# These are using some hooks which are from my mlworks branch,
# to set the default configuration on project open,
cat << EOF >~/.mlworks
local
  val defaultConfig = "I386/Linux";
  fun hasConfig(cfg) = List.foldr (fn (s, x as SOME _) => if s = cfg then NONE else SOME cfg
				    | (_,	 NONE) => NONE) (SOME cfg) (Shell.Project.showAllConfigurations());
  fun addConfig(SOME cfg) = Shell.Project.setConfigurationDetails(cfg, {files = [], library = []})
    | addConfig(NONE) = ();
  fun setConfig(cfg) =

ratmice

stream = fun 'a 'b =>
type (rec t => {
  hd : a;
  tl : alt (type {} -> t) (b)
});

;; whatever...
toString i = Text.fromChar (Char.fromInt (i + 48));

;; kind of a dumb example...

ratmice

#![allow(dead_code)]

mod sealer_unsealer {
    use std::rc::Rc;
    use std::ptr;

    pub struct Sealed<T> {
        value: T,
        brand: Rc<Brand>
    }