copumpkin

module Mat where

open import Function
open import Data.Empty
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin; zero; suc; toℕ)
open import Data.Fin.Props using ()
open import Data.Product
open import Relation.Nullary
open import Relation.Binary

supki

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}

puffnfresh

-- Idris translation of copumpkin's Agda code:
-- https://gist.github.com/copumpkin/8758586

-- Proves that List reverse is completely specified by:
-- 1. f [] = []
-- 2. f [x] = [x]
-- 3. f (xs ++ ys) = f ys ++ f xs

reverse' : List a -> List a
reverse' [] = []

ikedaisuke

Require Import Coq.Lists.List.

Lemma rev_Unfold : forall {A:Type} (l:list A) (a:A), rev (a::l) = rev l ++ (cons a nil).
Proof.
intros.
simpl.
reflexivity.
Qed.

Theorem rev_Involutive : forall {A:Type} (l:list A), rev (rev l) = l.

copumpkin

module Categories.Agda.State where

open import Categories.Category
open import Categories.Agda
open import Categories.Agda.Product
open import Categories.Functor hiding (_≡_)
open import Categories.Functor.Product
open import Categories.Functor.Hom
open import Categories.Monad
open import Categories.Adjunction

supki

#!/usr/bin/env perl
# This crappy perl script parses .cabal files for `authors' field and extracts authors names. Then it collects them in one enormous hash associating total number of findings. Then it "pretty"-prints hash from most productive authors to least productive.
use v5.14;
use warnings FATAL => qw(void);


# Skip all lines before /^author:/i one, then return it.
sub lex ($) {
	my $h = $_[0];
	while (<$h>) { if (/^author:/i) { return $_ } }

proger

helper = /tmp/.build-secrets-helper
# path to the ephemeral store
store = /run/sproxy-sink/store
aes_path = secrets/aes-password
gpg_key = C4DECDD2

secrets-encrypted: paths-sproxy.nix $(aes_path)
	tar c $(store) | openssl aes-256-cbc -pass file:secrets/aes-password -a > $@

paths-sproxy.nix: ./sproxy-config.nix

supki

{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE UnicodeSyntax #-}

import Data.Colour
import Diagrams.Prelude
import Diagrams.Backend.Cairo.CmdLine
import Graphics.Rendering.Diagrams.Points


main ∷ IO ()

TheEvilDev

class Dependency
    attr_accessor :Name, :Version

    def initialize(name, version)
        @Name = name
        @Version = version
    end
end

voidlizard

ghc -i -static -optl-static -optl-pthread -funbox-strict-fields -fwarn-incomplete-patterns -isrc --make Program.hs