palmskog

Positive vs. negative coinductive finiteness in Coq

Positive

siraben

xeeg

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

wenkokke

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

Blaisorblade

(coq.theory
 (name notation_test)

 (flags (:standard)))

rossabaker

import cats._

// A pure functional, contravariant monoidal string builder
sealed trait SB[A] {
  final def render(a: A): String = {
    val sb = new StringBuilder
    renderInternal(sb, a)
    sb.toString
  }

aaronmdjones

-----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

martinchapman

# 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

angerman

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

bobatkey

{-# 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