Kha

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)

lukaszlew

-- 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

/-
  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

{
/* 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