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). |
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 |
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 *) |
View knot.ml
let x = ref (fun z -> z) in | |
let f = fun z -> (!x) z in | |
x := f; f () | |
(* f () → (!x) () → f () → ... *) |
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)) |
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 |
NewerOlder