joom

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

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

{
  "~P" = (insertText:, "Π");
  "~s" = (insertText:, "ş");
  "~S" = (insertText:, "Ş");
  "~k" = (insertText:, "ı");
  "~K" = (insertText:, "İ");
  "~g" = (insertText:, "ğ");
  "~G" = (insertText:, "Ğ");
  "~l" = (insertText:, "λ");
  "~L" = (insertText:, "Λ");

joom

{-# 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

Inductive color := red | green | blue.

joom

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
module Scott where

joom

import System.Random

data Move = Rock | Paper | Scissors deriving (Show, Eq, Enum)

instance Ord Move where
  (<=) x y = x == y || (x,y) `elem` [(Rock,Paper),(Paper,Scissors),(Scissors,Rock)]

humanSelect :: IO Move
humanSelect = fmap (toEnum . read) getLine

joom

module SimplyTypedLambdaCalculus where

  open import Data.Bool
  open import Data.Nat hiding (erase)
  import Data.Unit
  open import Data.Maybe
  open import Data.Product
  open import Data.Sum
  open import Relation.Binary.PropositionalEquality hiding ([_])
  open import Relation.Nullary

joom

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

%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