Skip to content

Instantly share code, notes, and snippets.

🦊
^_^

Dan Frumin co-dan

🦊
^_^
  • Nijmegen
Block or report user

Report or block co-dan

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@co-dan
co-dan / poly.v
Created Sep 9, 2017
Encode-decode for the polynomials
View poly.v
Fixpoint code_poly (P Q : polynomial) : Type :=
match P, Q with
| poly_var, poly_var => Unit
| poly_const C, poly_const C' => C = C'
| poly_times Q R, poly_times Q' R' => (code_poly Q Q') * (code_poly R R')
| poly_plus Q R , poly_plus Q' R' => (code_poly Q Q') * (code_poly R R')
| _, _ => Empty
end.
View Map2.agda
module Map2 where
--------------------------------------------------
-- * Prelude
--------------------------------------------------
-- Taken from: https://github.com/pigworker/Ohrid-Agda
open import Ohrid-Prelude
open import Ohrid-Nat
-- Mini HoTT (Except that we have K)
View wellfounded.v
(** Well-founded relations in intuitionistic type theory *)
(** last updated : 5 of April, 2017. email: dfrumin [at] cs.ru.nl *)
Definition relation A := A -> A -> Prop.
Section wf.
Variable A : Type.
Variable R : relation A.
Notation "x '<' y" := (R x y).
(** * Intuitionistic well-foundedness criteria *)
@co-dan
co-dan / knot.ml
Last active Jan 20, 2017
Landin's knot
View knot.ml
let x = ref (fun z -> z) in
let f = fun z -> (!x) z in
x := f; f ()
(* f () → (!x) () → f () → ... *)
@co-dan
co-dan / interp.rkt
Created Jul 19, 2016
cbv λ-calculus interpreter with unbounded continuations
View interp.rkt
#lang racket
(require racket/dict) ;; for dict-lookup for env
; eval-apply interpreter for call-by-value λ-calculus with call/cc
; scroll down to test1, test2 and yin & yang to see example programs
(define id (lambda (x) x))
(define initev '())
(define (ext k v e)
(cons (cons k v) e))
@co-dan
co-dan / Dice.hs
Created Feb 22, 2015
A simple dice rolling bot based on `pipes-irc'. Responds to commands like "roll d20+d4+3"
View Dice.hs
{-# LANGUAGE OverloadedStrings #-}
import Control.Monad
import Control.Monad.Identity
import Control.Monad.Random
import qualified Data.ByteString as BS
import qualified Data.ByteString.Char8 as B
import Data.Maybe
import Data.Set as S
import Data.Traversable as T
import Pipes
View nat_well_founded.v
Require Import Rel.
Require Import Coq.Init.Wf.
Theorem nat_wo: well_founded lt.
Proof.
intro n.
assert (forall y x, x < y -> Acc lt x) as A.
induction y.
+ intros x H; inversion H.
+ intros x H'. apply Acc_intro.
View induction.v
Inductive gorgeous : nat -> Prop :=
g_0 : gorgeous 0
| g_plus3 : forall n, gorgeous n -> gorgeous (3+n)
| g_plus5 : forall n, gorgeous n -> gorgeous (5+n).
Fixpoint gorgeous_ind_max (P: forall n, gorgeous n -> Prop) (f : P 0 g_0)
(f0 : forall (m : nat) (e : gorgeous m),
P m e -> P (3+m) (g_plus3 m e))
(f1 : forall (m : nat) (e : gorgeous m),
P m e -> P (5+m) (g_plus5 m e))
(n : nat) (e: gorgeous n) : P n e :=
View Home.hs
{-# LANGUAGE OverloadedStrings #-}
module Controllers.Home (homeRoutes) where
import Web.Scotty
import Data.Monoid (mconcat)
import qualified Database.RethinkDB as R
import qualified Database.RethinkDB.NoClash
homeRoutes :: ScottyM ()
@co-dan
co-dan / gist:c874b9624ef09399a2c7
Last active Dec 17, 2017
Yoneda lemma for fmap fusion
View gist:c874b9624ef09399a2c7
--------------------------------------------------
-- Yoneda lemma
newtype Yoneda f a =
Yoneda (forall b. (a -> b) -> f b)
-- Nat (Hom(a, -), F) ~~ F a
-- this is `liftYoneda`
yoneda :: (Functor f) => f a -> Yoneda f a
yoneda x = Yoneda $ \f -> fmap f x
You can’t perform that action at this time.