Skip to content

Instantly share code, notes, and snippets.

View joom's full-sized avatar

Joomy Korkut joom

349 followers · 418 following
View GitHub Profile
@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] & & \\
@joom
joom / Unquote.idr
Last active May 21, 2018 12:58
module Unquote
%access public export
||| An interface to recover things from their canonical representations
||| as reflected terms, i.e. to reify things.
|||
||| This interface is intended to be used during proof
||| automation and the construction of custom tactics.
|||
||| @ t the type to quote it from (typically `TT` or `Raw`)
@joom
joom / Hints.idr
Last active March 28, 2018 06:07
Super hacky hint database for Idris.
||| Hacky and rudimentary hint database for Idris using elaborator reflection.
||| You can now write tactics that does `getHints`
||| and try to prove the goal with the lemmas there.
module Hints
import Language.Reflection.Utils
%language ElabReflection
%access public export
||| The hint to pass the machine generated names. Note that the word hint here
||| is used literally, not in the theorem prover sense.