Jon Sterling jonsterling
jonsterling
/ LOL.v
Created
September 23, 2017 04:08
This file has been truncated, but you can view the full file.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Nuprl_functional = | |
| λ _top_assumption_ : nat, | |
| (λ (_evar_0_ : (λ n : nat, matrix_functional (Nuprl n)) 0) | |
| (_evar_0_0 : ∀ n : nat, (λ n0 : nat, matrix_functional (Nuprl n0)) (S n)), | |
| match | |
| _top_assumption_ as n | |
| return ((λ n0 : nat, matrix_functional (Nuprl n0)) n) | |
| with | |
| | 0 => _evar_0_ |
jonsterling
/ recitation-source.tex
Created
September 17, 2017 20:23
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| \documentclass{article} | |
| \usepackage{libertine} | |
| \usepackage[usenames,dvipsnames,svgnames,table]{xcolor} | |
| \usepackage{amsmath, amssymb, proof, microtype, hyperref} | |
| \usepackage{mathpartir} % for mathpar, not for proofs | |
| \usepackage{perfectcut} | |
| \newcommand\Parens[1]{\perfectparens{#1}} | |
| \newcommand\Squares[1]{\perfectbrackets{#1}} |
jonsterling
/ gist:486673f7943f5ddce7c68d2389341f90
Last active
March 16, 2017 05:11
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module experiment where | |
| open import Agda.Primitive | |
| open import Prelude.List | |
| open import Prelude.Size | |
| open import Prelude.Monoidal | |
| open import Prelude.Monad | |
| open import Prelude.Functor | |
| open import Prelude.Natural | |
| open Size using (∞) |
jonsterling
/ lambda-nu.clf
Last active
December 22, 2016 00:45
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| id : type. | |
| id/z : id. | |
| id/s : id -o id. | |
| answer : type. | |
| yes : answer. | |
| no : answer. | |
| id/eq? : id -> id -> answer -> type. | |
| id/eq/z/z : id/eq? id/z id/z yes. |
jonsterling
/ anti-jondentation.lisp
Last active
November 12, 2016 22:30
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (my-long-op-name first-argument | |
| (something-else oh-boy | |
| here-we-go-again)) | |
| ;; I would prefer: | |
| (my-long-op-name | |
| first-argument | |
| (something-else | |
| oh-boy |
jonsterling
/ nextgen-dependent-lcf.sml
Last active
October 10, 2016 21:31
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| signature THEORY = | |
| sig | |
| type sort | |
| type term | |
| structure Var : | |
| sig | |
| include ORDERED | |
| val toString : t -> string | |
| end |
jonsterling
/ gist:c7e116221ed4c3dbace54c21dce3c108
Created
October 7, 2016 01:10
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Theorem foo : ⸤⊢ (n:nat) =(zero; succ(n); nat) -> =(zero; succ(n); nat)⸥ { | |
| fun-intro(n.fun-intro(x.x; eq⁼(nat-eq; zero-eq; succ-eq(hyp-eq(n)))); nat-eq) | |
| } ext { | |
| lam(_.lam(x.x)) | |
| }. | |
| Operator is-zero : (0). | |
| ⸤is-zero(n)⸥ ≝ ⸤natrec(n; unit; _._.void)⸥. | |
| Theorem succ-not-zero : ⸤⊢ (n:nat) =(succ(n); zero; nat) -> void⸥ { |
jonsterling
/ gist:475c91adef4ebe0457260a94a11aae51
Created
September 21, 2016 18:56
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (unless (package-installed-p 'use-package) | |
| (package-refresh-contents) | |
| (package-install 'use-package)) | |
| (require 'use-package) | |
| (defun jms-redprl-startup-hook () | |
| "Get flycheck running when RedPRL starts." | |
| (flycheck-mode) |
jonsterling
/ lcs.sml
Last active
May 27, 2016 01:31
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| signature LCS_SORT = | |
| sig | |
| structure AtomicSort : SORT | |
| type atomic = AtomicSort.t | |
| datatype t = | |
| VAL of atomic | |
| | KONT of atomic * atomic | |
| | CMD of atomic |
jonsterling
/ gist:55250d1dab5af9629e5695931368ca05
Created
May 24, 2016 01:32
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ENOENT: no such file or directory, open '.babelrc' | |
| Error: ENOENT: no such file or directory, open '.babelrc' | |
| at Error (native) | |
| at Object.fs.openSync (fs.js:549:18) | |
| at Object.fs.readFileSync (fs.js:397:15) | |
| at babelrc (/Users/jon/src/atom-language-redprl/node_modules/babelrc-rollup/dist/babelrc-rollup.js:14:47) | |
| at Object.<anonymous> (/Users/jon/src/atom-language-redprl/src/grammar-generator/rollup.config.js:22:11) | |
| at Module._compile (module.js:435:26) | |
| at Object.require.extensions..js (/Users/jon/src/atom-language-redprl/node_modules/rollup/bin/runRollup.js:54:8) | |
| at Module.load (module.js:356:32) |