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

%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

\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

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

||| 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.