{{ message }}

Instantly share code, notes, and snippets.

# Gergő Érdigergoerdi

Created Jul 25, 2017
View monitor.rs
 #![feature(lang_items)] #![feature(fundamental)] #![feature(intrinsics)] #![feature(on_unimplemented)] #![feature(optin_builtin_traits)] #![feature(unboxed_closures)] #![feature(associated_type_defaults)] #![feature(asm)] #![feature(abi_avr_interrupt)] #![feature(unwind_attributes)]
Created Feb 9, 2017
View ScopeCheckingLC.agda
 module _ where open import Function using (_∘_) open import Relation.Binary.PropositionalEquality open import Relation.Binary open import Relation.Nullary open import Data.Empty -- Untyped lambda calculus, with "weak" names module _ where
Last active May 1, 2018
View Printf.hs
 {-# LANGUAGE GADTs, TypeInType, DataKinds, TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeApplications #-} import GHC.TypeLits import GHC.Types import Data.Singletons import Data.Singletons.Prelude data Format = Lit Symbol | Str | Shown Type
Created Jun 22, 2016
View Fib.hs
 fib' :: (Integer, Integer) -> (Integer, Integer) -> Integer -> Integer fib' (p, q) (x0, x1) n = go n (p, q) (x0, x1) where go 0 (p, q) (x0, x1) = x0 go n (p, q) (x0, x1) = if odd then go (n-1) (p, q) \$! step (p, q) (x0, x1) else go n' (p', q') (x0, x1) where (n', b) = n `divMod` 2 odd = not (b == 0)
Last active Dec 23, 2015
View ParametrictyViaLFT.agda
 -- https://stackoverflow.com/questions/34388484/parametricity-exploiting-proofs-in-agda PolyFun : Set → Set1 PolyFun A = ∀ {X : Set} → A → X → A open import Relation.Binary.PropositionalEquality Parametricity : {A : Set} → Set _ Parametricity {A} = ∀ {X Y} → (f : PolyFun A) → ∀ a x y → f {X} a x ≡ f {Y} a y
Last active Dec 18, 2015
Canonical representation of polymorphic functions over containers (http://stackoverflow.com/a/34346484/477476)
View Shapeshifting.agda
 open import Data.Product open import Function using (_∘_; id) data Cont : Set₁ where _<|_ : (S : Set) → (P : S → Set) → Cont [_]C : Cont → Set → Set [ S <| P ]C X = Σ[ s ∈ S ] (P s → X)
Created Dec 4, 2015
View SystemF.agda
 open import Data.List open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′) renaming (map to mapSum) open import Function using (id; _∘_) open import Relation.Binary.PropositionalEquality Con : Set → Set Con = List data Var {A : Set} (t : A) : Con A → Set where here : ∀ {Γ : Con A} → Var t (t ∷ Γ)
Created Nov 12, 2015
View PermutationFunsHigherKinded.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 Permutation : Nat -> Type
Last active Nov 12, 2015
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)
Created Nov 11, 2015
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)
You can’t perform that action at this time.