This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#![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, |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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)⟩ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
### 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: |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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>, | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// 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>, | |
} |
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
NewerOlder