Skip to content

Instantly share code, notes, and snippets.

View joom's full-sized avatar

Joomy Korkut joom

474 followers · 450 following
View GitHub Profile
@joom
joom / post-it.tex
Created July 8, 2026 14:24
Post-it note in LaTeX
\usepackage{tcolorbox}
\tcbuselibrary{skins,breakable}
\newcommand{\myremarkfold}{%
\path[fill=tcbcolback!80!black]
([yshift=3mm]interior.south east) -- ++(-0.4,-0.1) -- ++(0.1,-0.2);
\path[draw=tcbcolframe,shorten <=-0.05mm,shorten >=-0.05mm]
([yshift=3mm]interior.south east) -- ++(-0.4,-0.1) -- ++(0.1,-0.2);
}
@joom
joom / list_ext.v
Created February 26, 2026 12:37
Folding a commutative idempotent function over a list respects extensional equality
From Stdlib Require Import List Relations Classes.RelationClasses Classes.Morphisms.
Definition list_ext A : relation (list A) := fun l l' => forall x, In x l <-> In x l'.
Class Associative {A : Type} (op : A -> A -> A) :=
assoc : forall x y z, op x (op y z) = op (op x y) z.
Class Commutative {A : Type} {B : Type} (op : A -> A -> B) :=
comm : forall x y, op x y = op y x.
@joom
joom / tree.rs
Last active August 18, 2023 02:40
A Yew app to show a binary tree
use yew::{html, Component, Context, Html};
use gloo::console::{self};
use std::collections::VecDeque;
#[derive(Debug, Clone)]
pub struct Annot {
}
impl Default for Annot {
fn default() -> Annot { Annot { } }
@joom
joom / .bash_profile
Created May 31, 2022 23:43
export BASH_SILENCE_DEPRECATION_WARNING=1
# https://github.com/dotzero/iTerm-2-Peppermint
git_branch () {
if git rev-parse --git-dir >/dev/null 2>&1
then echo -e "" [ $(git branch 2>/dev/null| sed -n '/^\*/s/^\* //p')]
else
echo ""
fi
}
function git_color {
@joom
joom / DefaultKeyBinding.dict
Created February 16, 2021 15:14
put it in ~/Library/KeyBindings on Mac systems
{
"~P" = (insertText:, "Π");
"~s" = (insertText:, "ş");
"~S" = (insertText:, "Ş");
"~k" = (insertText:, "ı");
"~K" = (insertText:, "İ");
"~g" = (insertText:, "ğ");
"~G" = (insertText:, "Ğ");
"~l" = (insertText:, "λ");
"~L" = (insertText:, "Λ");
@joom
joom / matchConstructor.hs
Last active December 8, 2020 22:21
Find out if a value matches a certain constructor.
{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
import Data.Data
import Unsafe.Coerce
type family Last (a :: *) :: * where
Last (b -> c) = Last c
Last d = d
full :: (Typeable a, Data (Last a)) => a -> Last a
full x = case typeRepArgs (typeOf x) of
@joom
joom / A.v
Created September 21, 2019 02:13
Coq extraction in separate modules
Inductive color := red | green | blue.
@joom
joom / Scott.hs
Last active February 27, 2019 13:19
Automatically going back and forth between a Haskell value and its Scott encoding, using Data and Typeable. For more explanation, look for my work on "Direct Reflection for Free!"
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
module Scott where
@joom
joom / SatisfyPairs.idr
Last active April 27, 2018 15:18
%language ElabReflection
data SatisfyPairs : (a -> a -> Type) -> List a -> Type where
SatEmpty : SatisfyPairs p []
SatSingleton : SatisfyPairs p [x]
SatPair : p x y -> SatisfyPairs p (y :: ys) -> SatisfyPairs p (x :: y :: ys)
MonotonicallyIncreasingNat : List Nat -> Type
MonotonicallyIncreasingNat = SatisfyPairs LTE
@joom
joom / lambda-cube.tex
Created April 14, 2018 02:03
Barendregt's lambda cube in tikzcd, with labels on arrows
\documentclass{standalone}
\usepackage{tikz-cd}
\usepackage{amsmath}
\usepackage{tgpagella}
\begin{document}
\begin{tikzcd}
& & \lambda\omega \arrow[rrr] & & & \lambda\Pi\omega \\
& & & & & \\
\lambda 2 \arrow[rruu] \arrow[rrr] & & & \lambda\Pi 2 \arrow[rruu] & & \\