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
View list.v.diff
diff --git a/theories/list.v b/theories/list.v
index 2f1db8e..a200405 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2988,6 +2988,11 @@ Section setoid.
Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
Global Instance list_lookup_proper i : Proper ((≡@{list A}) ==> (≡)) (lookup i).
Proof. induction i; destruct 1; simpl; try constructor; auto. Qed.
+ Global Instance list_lookup_total_proper `{!Inhabited A} i :
+ Proper ((≡@{list A}) ==> (≡)) (lookup_total i).
@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 ()
You can’t perform that action at this time.