Skip to content

Instantly share code, notes, and snippets.

View HuStmpHrrr's full-sized avatar

Jason Hu HuStmpHrrr

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 / 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 / stlc.v
Last active September 10, 2018 16:55
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.
induction m.
- intros vec. exact vec.
- intros vec. inversion vec; subst.
apply IHm. apply X.
View coq-debug-eauto.el
(defun coq-debug-eauto-output--transform (flag)
(goto-char (line-beginning-position))
(let ((line (buffer-substring-no-properties
(pcase line
("" nil)
("Debug: (* debug eauto: *)"
(delete-region (line-beginning-position) (line-end-position))
#!/usr/bin/env python
# vim: ft=python
import bs4
import cgitb
import os
import sys