Skip to content

Instantly share code, notes, and snippets.

Avatar

Gergő Érdi gergoerdi

View GitHub Profile
View PermutationFuns.idr
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)
View Permutations.idr
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)
View ToggleSync.vhdl
-- 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;
View SymIterComplete.agda
-- 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
gergoerdi / SymIter.agda
Last active Aug 29, 2015
Defining commutative functions
View SymIter.agda
-- 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
gergoerdi / irreducible.agda
Last active Aug 29, 2015
Irreducibility vs. primality
View irreducible.agda
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
View STLC.hs
{-# 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
View families-open.hs
{-
- 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 #-}
View families-closed-datakinds.hs
{-
- Instant Insanity using Closed Type Families and DataKinds.
-
- See: http://stackoverflow.com/questions/26538595
-}
{-# OPTIONS_GHC -ftype-function-depth=400 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
View families-closed.hs
{-
- Instant Insanity using Closed Type Families.
-
- See: http://stackoverflow.com/questions/26538595
-}
{-# OPTIONS_GHC -ftype-function-depth=400 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}