ratmice

#![allow(dead_code)]

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

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

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

# 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

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

  val v = {};

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

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

namespace hidden

variables {A B C : Type}
open function

-- From chapter 16, but has no implementation in the lean function namespace.
theorem surjective_of_right_inverse {g : B  → A} {f : A → B} :
  right_inverse g f → surjective f :=
assume h, assume y,
let  x : A := g y in

ratmice

open function

variables {α β : Type}
def inverse (g : β → α) (f : α → β) := left_inverse g f ∧ right_inverse g f
def inverse_comp (f : α → β) (g : β → α) (gf_inv : inverse g f)
  : (∀ a, (g ∘ f) a = a) ∧ (∀ b, (f ∘ g) b = b) :=
    ⟨gf_inv.left, gf_inv.right⟩

  def inverse_comp_id {f : α → β} {g : β → α} (gf_inv  : inverse g f)
  : (g ∘ f = id) ∧ (f ∘ g = id)

ratmice

ratmice

// Requires druid features = ["im"]
// And I *think* druid from git.
use im;
use druid::{self, lens, Data,
    widget::{Flex, List, Scroll, Widget, WidgetExt, Slider, ListIter}};

#[derive(Clone, Data, Debug)]
struct AppState {
    state: im::HashMap<String, f64>,
}