gergoerdi

import Data.Vect
import Data.Fin

%default total

fins : Vect n (Fin n)
fins {n = Z} = []
fins {n = S n} = FZ :: map FS fins

permutations : {n : Nat} -> Vect (fact n) (Vect n a -> Vect n a)

gergoerdi

import Data.Vect

%default total

permutations : Vect n a -> Vect (fact n) (Vect n a)
permutations [] = [[]]
permutations {n = S n} (x :: xs) = rewrite multCommutative (S n) (fact n) in
                                   concat $ map (inserts x) (permutations xs)
  where
    inserts : a -> Vect k a -> Vect (S k) (Vect (S k) a)

gergoerdi

-- Based on http://www.edn.com/electronics-blogs/day-in-the-life-of-a-chip-designer/4435339/Synchronizer-techniques-for-multi-clock-domain-SoCs
-- via http://electronics.stackexchange.com/questions/182331/

library IEEE;
use IEEE.STD_LOGIC_1164.ALL;

entity ToggleSync is
    Port ( CLK_FAST_SOURCE : in  STD_LOGIC;
           CLK_SLOW_TARGET : in  STD_LOGIC;
           PULSE_IN : in  STD_LOGIC;

gergoerdi

-- continued from https://gist.github.com/gergoerdi/46ad83513fd9db65c286

module Complete where
  open import Data.Product

  record SymItery {X Y : Set} : Set where
    constructor SymIter
    field
      zen : ℕ → X
      more : X → X

gergoerdi

-- From Conor McBride: https://lists.chalmers.se/pipermail/agda/2015/007768.html
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Function

symIter : {X : Set} → (ℕ → X) → (X → X) → ℕ → ℕ → X
symIter zen more zero    y       = zen y
symIter zen more x       zero    = zen x
symIter zen more (suc x) (suc y) = more $ symIter zen more x y

gergoerdi

open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum
open import Data.Nat

data Irreducible (n : ℕ) : Set where
  irreducible : n ≢ 1 → (∀ x y → n ≡ x * y → x ≡ 1 ⊎ y ≡ 1) → Irreducible n

open import Data.Nat.Primality

gergoerdi

{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
module STLC where

import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Type.Equality

gergoerdi

{-
 - Instant Insanity using Type Families.
 -
 - See:  The Monad Read, Issue #8 - http://www.haskell.org/wikiupload/d/dd/TMR-Issue8.pdf
 -}

{-# OPTIONS_GHC -ftype-function-depth=400 #-}

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}

gergoerdi

{-
 - Instant Insanity using Closed Type Families and DataKinds.
 -
 - See:  http://stackoverflow.com/questions/26538595
 -}

{-# OPTIONS_GHC -ftype-function-depth=400 #-}

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}

gergoerdi

{-
 - Instant Insanity using Closed Type Families.
 -
 - See:  http://stackoverflow.com/questions/26538595
 -}

{-# OPTIONS_GHC -ftype-function-depth=400 #-}

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}