Skip to content

Instantly share code, notes, and snippets.

Avatar
🐈
=^_^=

Dan Frumin co-dan

🐈
=^_^=
  • Groningen
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 / 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
@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 / .zshrc
Last active Dec 31, 2015
Cabal sandbox status in your ZSH prompt
View .zshrc
#
# This simple script displays whether you are in a cabal sandbox
# the the result of checking for a sandbox is cached, but now that I
# actually think about it, it was probably an unnecessary step.
# Don't forget to customize the PROMPT variable at the bottom
#
# Looks like this with my prompt: https://files.app.net/rjphjAG9.png
#
function update_cabal_sandbox_info () {
View gist:7945382
Resolving dependencies...
Configuring diagrams-contrib-1.0.0.1...
Building diagrams-contrib-1.0.0.1...
Preprocessing library diagrams-contrib-1.0.0.1...
src/Diagrams/TwoD/Tilings.hs:94:39:
warning: missing terminating ' character [-Winvalid-pp-token]
-- Instead of using Doubles, which can't be compared for equality, it
^
View interactive.hs
{-# LANGUAGE TypeFamilies,
MultiParamTypeClasses,
FlexibleInstances,
UndecidableInstances,
FunctionalDependencies #-}
import Control.Concurrent
import Control.Monad
import Control.Monad.Fix
import JavaScript.JQuery