Skip to content

Instantly share code, notes, and snippets.

View HuStmpHrrr's full-sized avatar
🎯
Focusing

Jason Hu HuStmpHrrr

🎯
Focusing
View GitHub Profile
View Dinatural.agda
open import Level
open import Data.Product
open import Categories.Category
open import Categories.NaturalTransformation as NT
open import Categories.Functor
open import Categories.Functor.Bifunctor
open import Categories.Category.Product
import Categories.Square as Square
@HuStmpHrrr
HuStmpHrrr / bug.v
Last active October 23, 2018 02:01
Equations bug
View bug.v
From Equations Require Import Equations.
Require Import Equations.Subterm.
Require Import Lia.
Section Tests.
Variable A : Type.
Inductive forest : Type :=
| emp : A -> forest
@HuStmpHrrr
HuStmpHrrr / stlc.v
Last active September 10, 2018 16:55
STLC
View stlc.v
Set Implicit Arguments.
Require Import Coq.Lists.List.
Require Import PeanoNat.
Require Import FunInd.
Require Import Arith.Wf_nat.
Require Import Recdef.
Require Import Omega.
View Matrix.v
Require Import Coq.Vectors.Vector.
Definition drop {A} {m n} : Vector.t A (m + n) -> Vector.t A n.
Proof.
induction m.
- intros vec. exact vec.
- intros vec. inversion vec; subst.
apply IHm. apply X.
Defined.
View coq-debug-eauto.el
(defun coq-debug-eauto-output--transform (flag)
(goto-char (line-beginning-position))
(let ((line (buffer-substring-no-properties
(line-beginning-position)
(line-end-position))))
(pcase line
("" nil)
("Debug: (* debug eauto: *)"
(delete-region (line-beginning-position) (line-end-position))
View ghc-libs-doc.py
#!/usr/bin/env python
# vim: ft=python
import bs4
import cgitb
import os
import sys
cgitb.enable()