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 / 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
You can’t perform that action at this time.