ncfavier

open import 1Lab.Path
open import 1Lab.Path.Groupoid
open import 1Lab.Type
open import 1Lab.Equiv

data Susp {ℓ} (A : Type ℓ) : Type ℓ where
  N S   : Susp A
  merid : A → N ≡ S

data Join {ℓ₁ ℓ₂} (A : Type ℓ₁) (B : Type ℓ₂) : Type (ℓ₁ ⊔ ℓ₂) where

ncfavier

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Function.Base
open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import Data.Sum

data Bin : Set where
  ⟨⟩ : Bin

ncfavier

module Lib (shortestLongest) where

import Control.Applicative
import Data.Maybe

steps = go []
  where
    go l (x:xs) = Nothing : go (x:l) xs
    go l [] = Just [reverse l] : repeat (Just [])

ncfavier

Require Import Arith ZArith Lia List Ascii String Program.Basics.
Open Scope string_scope.
Open Scope program_scope.
Import ListNotations.

(** The head character of a string, returned as a new string.
   If the string is empty, returns the empty string. *)

Definition head s := match s with
  | "" => ""

ncfavier

{-# LANGUAGE LambdaCase #-}
module SevenTreesInOne where
import Test.QuickCheck

infixl :*
data T = O | T :* T
  deriving (Eq, Ord, Show)

type T7 = (T, T, T, T, T, T, T)

ncfavier

#!/usr/bin/env -S nix-instantiate --eval --strict
# real  0m4.143s
with (builtins.getFlake "nixos").lib;
let
  tails = l: if l == [] then [] else [ l ] ++ tails (tail l); 
  sum = foldl' (x: y: x + y) 0;
  product = foldl' (x: y: x * y) 1;
  lines = s: splitString "\n" (removeSuffix "\n" s); 

  nums = map toInt (lines (builtins.readFile ./input1));

ncfavier

#!/usr/bin/env bash
# dependencies: bash 4+, jq

. ./config.sh
: "${verbose:=0}"
: "${syncplay_host:=syncplay.pl}"
: "${syncplay_port:=8999}"
: "${syncplay_nick:=syncplaybridge}"
: "${syncplay_room:?"can't be empty"}"
: "${irc_host:=chat.freenode.net}"

ncfavier

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ImpredicativeTypes #-} -- HIGHLY EXPERIMENTAL
import           Data.Map (Map)
import qualified Data.Map as Map
import           Data.Function

-- Say we want to define this function:
mergeKeys :: Map k a -> Map k b -> [k]

{- The obvious implementation is of course

ncfavier

traverse   :: (Traversable t, Applicative f) => (a -> f b) -> t a        -> f (t b)
traverse_  :: (Foldable    t, Applicative f) => (a -> f b) -> t a        -> f ()
for        :: (Traversable t, Applicative f) => t a        -> (a -> f b) -> f (t b)
for_       :: (Foldable    t, Applicative f) => t a        -> (a -> f b) -> f ()
sequenceA  :: (Traversable t, Applicative f) => t (f a)                  -> f (t a)
sequenceA_ :: (Foldable    t, Applicative f) => t (f a)                  -> f ()
mapM       :: (Traversable t, Monad       m) => (a -> m b) -> t a        -> m (t b)
mapM_      :: (Foldable    t, Monad       m) => (a -> m b) -> t a        -> m ()
forM       :: (Traversable t, Monad       m) => t a        -> (a -> m b) -> m (t b)

ncfavier

#!/usr/bin/env bash

channel=$1

while read -rd ' ' time && read -rd ' ' event && IFS= read -r message; do
    time=${time#[} time=${time%]}
    case $event in
        '***')
            if [[ $message =~ ^(.*)' is now known as '(.*)$ ]]; then
                event='*'