ratmice

#![allow(unused)]
use kurbo::{Affine, Point, Rect, Shape, Stroke};
use vello::peniko::{BlendMode, BrushRef, Fill};
use vello::SceneBuilder;

#[derive(Clone)]
pub enum ShapeOp<'a, 'b> {
    Fill {
        style: Fill,
        transform: Affine,

ratmice

-- From the post https://dylanj.xyz/posts/rust-coq-opaque-types/
-- Figured it would be fun to do a lean version without tactics.
def impl_trait_transform (Trait: Type → Prop) (Result: Prop) :
  ((∃ t, Trait(t)) → Result) ↔ (∀ t, (Trait(t) → Result)) := 
    ⟨λ existsTrait, λ ty, λ trait, existsTrait ⟨ty, trait⟩,
     λ anyTrait, λ existsTrait, exists.elim existsTrait (λ ty, anyTrait ty)⟩

ratmice

#!/bin/sh
alias wezterm=~/.cargo/bin/wezterm

if [ $(swaymsg -t get_tree | jq '.. | select(.type?) | select(.focused==true and .window_properties.class == "org.wezfurlong.wezterm").window_properties.class, select(.focused==true and .app_id =="org.wezfurlong.wezterm").app_id') ];
  then
          PANE_ID=$(wezterm cli list-clients --format json | jq '.[] | .focused_pane_id')
          WORKDIR=$(wezterm cli list --format json | jq -r ".[] | select(.pane_id == $PANE_ID).cwd")
          wezterm cli spawn --new-window --cwd ${WORKDIR#file://}
     false
  else

ratmice

### Keybase proof

I hereby claim:

  * I am ratmice on github.
  * I am ratmice (https://keybase.io/ratmice) on keybase.
  * I have a public key ASBaC0vZKv1rdOPJWiCvEidXHYbm9ul_h2_mDHfaLlEa4Qo

To claim this, I am signing this object:

ratmice

use druid::widget::{Flex, Label};
use druid::{Data, Env, LocalizedString, Menu, MenuItem, Widget};
use druid_widget_nursery::{
    prism::{Closures, Prism},
    MultiRadio,
};
use im::Vector;
use std::collections::BTreeMap;
use std::sync::Arc;

ratmice

use druid::widget::ListIter;
use druid::Data;
use druid::im::Vector;

#[derive(Data, Clone)]
pub struct ListMod<I, T>
{
    data: I,
    mod_elems: Vector<T>,
}

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>,
}

ratmice

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

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