Skip to content

Instantly share code, notes, and snippets.

William J. Bowman wilbowma

Block or report user

Report or block wilbowma

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View subst.v
Require Import Omega.
Require Import Coq.Lists.ListSet.
Require Import Coq.Program.Wf.
Open Scope list.
Parameter atom : Type.
Parameter atomeq_dec : forall x y : atom, {x = y} + {x <> y}.
Notation "a '==' b" := (atomeq_dec a b) (at level 10).
wilbowma / meow1.v
Last active Sep 6, 2019
Test files for quickchick
View meow1.v
Require Import Strings.String.
Require Import Strings.Ascii.
Open Scope string_scope.
Require Import Bool.
Require Import Omega.
Require Import Nat.
Require Import ssreflect.
View meow.tex
% Play with xshift and yshift if it looks funny
\newcommand{\tikzmark}[1]{\tikz[overlay,remember picture,xshift=-3pt,yshift=1pt] \node (#1) {};}
wilbowma / in-digits.rkt
Last active May 28, 2019
A library for set!-ing numbers. You shouldn't use this.
View in-digits.rkt
#lang racket
;; int -> sequence
(define (in-digits int)
;; Manually do loop once to get 0 right.
(let-values ([(q r) (quotient/remainder int 10)])
(let loop ([i q]
[ls (cons r '())])
(if (zero? i)
wilbowma /
Created Oct 21, 2018 — forked from pwnsdx/
Disable bunch of #$!@ in Sierra (Version 2.1)
# IMPORTANT: You will need to disable SIP aka Rootless in order to fully execute this script, you can reenable it after.
# WARNING: It might disable things that you may not like. Please double check the services in the TODISABLE vars.
# Get active services: launchctl list | grep -v "\-\t0"
# Find a service: grep -lR [service] /System/Library/Launch* /Library/Launch* ~/Library/LaunchAgents
# Agents to disable
TODISABLE=('' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '
View stxutils.rkt
#lang racket/base
(for-template (only-in racket/base let-values #%plain-lambda))
View meow.rkt
(define-syntax (typed-axiom syn)
(syntax-parse syn
#:datum-literals (:)
#:with c (format-id syn "constant:~a" #'name #:source #'name)
#:with name- (format-id syn "~a-" #'name #:source #'name)
[(_:id name:id : type)
(define name-ls (parse-telescope-names #'type))
(define type-ls (parse-telescope-types #'type))
(define result (parse-telescope-result #'type))
View baseline.log
(quasiquote ((bd y y))):
cpu time: 320 real time: 317 gc time: 0
cpu time: 360 real time: 360 gc time: 0
cpu time: 667 real time: 667 gc time: 21
cpu time: 516 real time: 515 gc time: 19
wilbowma / remode.rkt
Last active May 25, 2017
Some macros for remoding a Redex judgment form. This is useful for testing I/O judgment forms, without worrying about how patterns and variables work together.
View remode.rkt
#lang racket/base
(only-in redex/private/term-fn judgment-form-mode)
(only-in racket/syntax format-id))
View fix-redex-judgment-indentation.el
;; fix indentation of inference rules with no hypothesis in Redex
(defun add-hyphens-as-racket-function (number-of-hyphens)
(when (> number-of-hyphens 1)
(put (intern (make-string number-of-hyphens ?-)) 'racket-indent-function
(lambda (state indent-point normal-indent)
(goto-char (elt state 1))
(list (1+ (current-column)) (elt state 1))))
(add-hyphens-as-racket-function (1- number-of-hyphens))))
(add-hyphens-as-racket-function 102)
You can’t perform that action at this time.