Skip to content

Instantly share code, notes, and snippets.

View Blaisorblade's full-sized avatar

Paolo G. Giarrusso Blaisorblade

191 followers · 191 following
View GitHub Profile
@Blaisorblade
Blaisorblade / dune
Last active November 27, 2021 20:17
Evidence for https://github.com/coq/coq/issues/15255; build by clone + dune build
(coq.theory
(name notation_test)
(flags (:standard)))
@Blaisorblade
Blaisorblade / opaque-opaque.v
Created October 29, 2021 23:34
From Coq Require Import Vector.
Lemma foo : nat.
Proof. exact 1. Qed.
Eval compute in foo.
Eval vm_compute in foo.
Lemma bar : nat.
Proof. exact 1. Defined.
@Blaisorblade
Blaisorblade / coqrc.v
Created October 19, 2021 13:11
My coqrc for development
Require Import Ltac.
Require Import ssreflect.
#[global] Set Nested Proofs Allowed.
#[global] Set Ltac Backtrace.
#[global] Unset SsrIdents.
@Blaisorblade
Blaisorblade / SB.scala
Created October 1, 2021 14:57 — forked from rossabaker/SB.scala
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
}
@Blaisorblade
Blaisorblade / interp.hs
Created September 18, 2021 17:29
Quick implementation of CBV evaluation for lambda calculus + some primitives + fix.
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Main where
{- Quick implementation of CBV evaluation for lambda calculus + some primitives + fix. -}
data BinOp = Add | Mul
deriving Show
evalBinOp :: BinOp -> Int -> Int -> Int
evalBinOp Add = (+)
evalBinOp Mul = (*)
@Blaisorblade
Blaisorblade / prop_nat.v
Created August 18, 2021 06:45
Induction on propositionally proof-irrelevant naturals
Require Import Coq.Program.Tactics.
Require Import Coq.Unicode.Utf8.
Require Import Coq.Logic.ProofIrrelevance.
Module prop_nat.
Inductive N : Prop := Z : N | S : N -> N.
(* Auto-generated. *)
Fixpoint N_ind' {P : Prop} (z : P) (s : N -> P -> P) (n : N) : P :=
match n with
@Blaisorblade
Blaisorblade / build-normal.txt
Last active April 30, 2021 21:12
$ dune build --cache=disabled --display=verbose theories/lang/prelude/notations.vo &> build-normal
Workspace root: /Users/pgiarrusso/git-bedrock/Coq/cpp2v-core
disable binary cache
Running[0]: /Users/pgiarrusso/.opam/iris-2021-01-12.0.bbaf3eaf-coq-8.13.0/bin/ocamlc.opt -config > /var/folders/7v/g2sr0z2s2v9d_v7xv_y1zlz00000gn/T/dune6d84c5.output
Dune context:
{ name = "default"
; kind = "default"
; profile = Dyn
; merlin = true
; for_host = None
@Blaisorblade
Blaisorblade / victory.v
Created December 15, 2020 15:39
Require Import NArith ZArith PArith.
Ltac is_positive p :=
lazymatch p with
| xI ?pa => is_positive pa
| xO ?pa => is_positive pa
| xH => idtac
| _ => fail
end.
Ltac is_N n :=
@Blaisorblade
Blaisorblade / oddity.txt
Created August 27, 2020 06:23 — forked from paulp/oddity.txt
Whitespace Oddity
WHITESPACE ODDITY
by Paul Phillips, in eternal admiration of David Bowie, RIP
Bound Ctrl to Major mode
Bound Ctrl to Major mode
Read inputrc and set extdebug on
Bound Ctrl to Major mode (Ten, Nine, Eight, Seven, Six)
Connecting readline, options on (Five, Four, Three)
Check the syntax, may terminfo be with you (Two, One, Exec)
@Blaisorblade
Blaisorblade / The Signs of Soundness
Created August 27, 2020 06:23 — forked from paulp/The Signs of Soundness
The Signs of Soundness
Hello scala, my old friend
I've come to take you home again
Because a feature slowly creeping
left me plagued with doubts and weeping
and the version that was tagged in the repo
just has to go
it lacks the signs of soundness
On sleepless nights I hacked alone
applying ant and other tools of stone