Paolo G. Giarrusso Blaisorblade

Positive vs. negative coinductive finiteness in Coq

Positive

Bionic Reader Bookmarklet

This bookmarklet is inspired by Bionic Reader API that is truly incredible. However I have issues with service APIs that are not clear on how they handle the privacy and security of my data. So I made a quick and dirty bookmarklet to do the job locally.

Create a new bookmark in your browser
Use this script as the address:

javascript:(function(){!function(){window.hasOwnProperty("bionicWordWrapApplied")||(!function(e){var n,t=document.createTreeWalker(e,NodeFilter.SHOW_TEXT,null,null);for(;n=t.nextNode();){for(var o,r=n.parentNode,d=n.nodeValue;o=d.match(/^(\s*)(\S+)/);){d=d.slice(o[0].length),r.insertBefore(document.createTextNode(o[1]),n);var a=Math.ceil(o[2].length/2),c=r.insertBefore(document.createElement("b"),n);c.appendChild(document.createTextNode(o[2].slice(0,a)));var i=r.insertBefore(document.createElement("span"),n);i.appendChild(document.createTextNode(o[2].slice(a)))}n.nodeValue=d}}(document.body),window.bionicWordWrapApplied=!0

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.

Glossary

When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:

_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3

Give Up GitHub

This project has given up GitHub. (See Software Freedom Conservancy's Give Up GitHub site for details.)

You can now find this project at paste.rossabaker.com instead.

Any use of this project's code by GitHub Copilot, past or present, is done without our permission. We do not consent to GitHub's use of this project's code in Copilot.

The nixos.org website suggests to use:

sh <(curl -L https://nixos.org/nix/install)

For macOS on Intel (x86_64) or Apple Silicon (arm64) based macs, we need to use

sh <(curl -L https://nixos.org/nix/install) --darwin-use-unencrypted-nix-store-volume

	-----BEGIN PGP SIGNED MESSAGE-----
	Hash: SHA512

	My resignation from freenode staff
	==================================

	I joined the freenode staff in March 2019 [1].

	Before I joined the staff, Freenode Ltd was sold [2] to a person named
	Andrew Lee as part of a sponsorship deal. The informal terms of that

	# Visualise a latex document git history

	# loop through commits, create a PDF from your main file for each
	# translate the pages of that PDF to a single image
	# create GIF/mp4 from the folder of images created

	# run within your local repository
	# prerequisites: ImageMagick and FFmpeg

	# create output folder

	{-# OPTIONS --rewriting #-}

	module cont-cwf where

	open import Agda.Builtin.Sigma
	open import Agda.Builtin.Unit
	open import Agda.Builtin.Bool
	open import Agda.Builtin.Nat
	open import Data.Empty
	import Relation.Binary.PropositionalEquality as Eq

	(coq.theory
	(name notation_test)

	(flags (:standard)))