Skip to content

Instantly share code, notes, and snippets.

View HuStmpHrrr's full-sized avatar

Jason Hu HuStmpHrrr

View GitHub Profile
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
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
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.
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.
(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