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
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
\documentclass{article}
\usepackage{mathpartir}
\usepackage{tikz}
% Play with xshift and yshift if it looks funny
\newcommand{\tikzmark}[1]{\tikz[overlay,remember picture,xshift=-3pt,yshift=1pt] \node (#1) {};}
\begin{document}
\[
@wilbowma
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)
ls
@wilbowma
wilbowma / disable.sh
Created Oct 21, 2018 — forked from pwnsdx/disable.sh
Disable bunch of #$!@ in Sierra (Version 2.1)
View disable.sh
#!/bin/bash
# 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=('com.apple.security.keychainsyncingoveridsproxy' 'com.apple.personad' 'com.apple.passd' 'com.apple.screensharing.MessagesAgent' 'com.apple.CommCenter-osx' 'com.apple.Maps.mapspushd' 'com.apple.Maps.pushdaemon' 'com.apple.photoanalysisd' 'com.apple.telephonyutilities.callservicesd' 'com.apple.AirPlayUIAgent' 'com.apple.AirPortBaseStationAgent' 'com.apple.CalendarAgent' 'com.apple.DictationIM' 'com.apple.iCloudUserNotifications' 'com.apple.familycircled' 'com.apple.familycontrols.useragent' 'com.apple.familynotificationd' 'com.apple.gamed' 'com.apple.icloud.findmydeviced.findmydevi
View stxutils.rkt
#lang racket/base
(require
(for-syntax
racket/base
syntax/parse
racket/syntax)
(for-template (only-in racket/base let-values #%plain-lambda))
racket/function
racket/match
syntax/id-set
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
Microbenchmarks
(quasiquote ((bd y y))):
noop-match:
cpu time: 320 real time: 317 gc time: 0
manual:freshen-match:
cpu time: 360 real time: 360 gc time: 0
binding:freshen-match:
cpu time: 667 real time: 667 gc time: 21
binding:freshen-skip-internal-match:
cpu time: 516 real time: 515 gc time: 19
@wilbowma
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
(require
redex/reduction-semantics
(for-syntax
racket/base
syntax/parse
(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.