Skip to content

Instantly share code, notes, and snippets.

View JasonGross's full-sized avatar

Jason Gross JasonGross

186 followers · 11 following
View GitHub Profile
@digama0
digama0 / fiat-test.lean
Last active November 2, 2019 04:00
Using simp and norm_num for big computations
import tactic.norm_num
import algebra.group_power
open prod
universes u v w ℓ
inductive let_bound (α : Type*)
| base : α → let_bound
| dlet : ℤ → (ℤ → let_bound) → let_bound
| mlet {β : Type} : β → (β → let_bound) → let_bound
open let_bound
@JasonGross
JasonGross / update_record.v
Created November 29, 2018 20:40
Record updating notations
Definition marker {T} (v : T) := v.
Ltac apply_with_underscores f x :=
match constr:(Set) with
| _ => constr:(f x)
| _ => apply_with_underscores uconstr:(f _) x
@JasonGross
JasonGross / html-scrape-classes.html
Last active November 3, 2020 17:50
Scrapers for Splash classes for 2015, in a combination of python and javascript
<html>
<!--// run `python -m SimpleHTTPServer 8000`, and visit http://localhost:8000/html-scrape-classes.html-->
<!--// run `python3 -m http.server 8000`, and visit http://localhost:8000/html-scrape-classes.html-->
<head>
<script type="text/javascript">
// follow the instructions at https://developers.google.com/google-apps/calendar/quickstart/js, using this in place of the quickstart file
// the output of the following javascript, run in the chrome console on https://esp.mit.edu/teach/Splash/2015/teacherreg, below
/*
var forPython = false;
var splashYear;// = 2016;