View Dinatural.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
View bug.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
From Equations Require Import Equations. | |
Require Import Equations.Subterm. | |
Require Import Lia. | |
Section Tests. | |
Variable A : Type. | |
Inductive forest : Type := | |
| emp : A -> forest |
View stlc.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/usr/bin/env python | |
# vim: ft=python | |
import bs4 | |
import cgitb | |
import os | |
import sys | |
cgitb.enable() |