Skip to content

Instantly share code, notes, and snippets.

View arademaker's full-sized avatar
🎯
Focusing

Alexandre Rademaker arademaker

🎯
Focusing
View GitHub Profile
@Kha
Kha / AesopSort.lean
Last active June 27, 2022 11:08
Lean 4 port of [Proving insertion sort correct easily in Coq](https://gist.github.com/siraben/3fedfc2c5a242136a9bc6725064e9b7d) using https://github.com/JLimperg/aesop
import Aesop
variable [LE α] [DecidableRel ((· ≤ ·) : α → α → Prop)]
@[aesop safe constructors]
inductive Sorted : List α → Prop where
| nil : Sorted []
| single : Sorted [x]
| cons_cons : x ≤ x' → Sorted (x' :: xs) → Sorted (x :: x' :: xs)
-- Based on: http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html
import Data.List (delete, union)
{- HLINT ignore "Eta reduce" -}
-- File mnemonics:
-- env = typing environment
-- vid = variable identifier in Bind or Var
-- br = binder variant (Lambda or Pi)
-- xyzTyp = type of xyz
-- body = body of Lambda or Pi abstraction
@brendanzab
brendanzab / maps.lean
Last active February 10, 2021 12:15
Total and partial maps in Lean 4 (inspired by Software Foundations)
/-
Total and partial maps
This is inspired by [the relevant chapter in Software Foundations]. Unlike
Software Foundations, these maps are also parameterised over a `Key`
type, which must supply an implementation of `DecidableEq`.
[Software Foundations]: https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html
-/
namespace Maps
@jwreagor
jwreagor / EmacsKeyBinding.dict
Created March 20, 2014 18:41
Global Emacs Key Bindings for OS X
{
/* Keybindings for emacs emulation. Compiled by Jacob Rus.
*
* This is a pretty good set, especially considering that many emacs bindings
* such as C-o, C-a, C-e, C-k, C-y, C-v, C-f, C-b, C-p, C-n, C-t, and
* perhaps a few more, are already built into the system.
*
* BEWARE:
* This file uses the Option key as a meta key. This has the side-effect
* of overriding Mac OS keybindings for the option key, which generally