digama0

universes i j k l m

def empty.elim (A : Sort i) (H : empty) : A :=
@empty.rec (λ e, A) H

def iso0 {A} {C : (empty → A) → Sort i} (f : empty → A) (H : C (empty.elim A)) : C f :=
eq.rec H (funext (empty.rec _) : empty.elim A = f)

def iso1 {A} {C : (unit → A) → Sort i} (f : unit → A) (H : C (λu, f ())) : C f :=
eq.rec H (funext (λu, unit.rec rfl u) : (λu, f ()) = f)

digama0

import system.io

universes u v

namespace hide

inductive format.color
| red | green | orange | blue | pink | cyan | grey

inductive format : Type

digama0

universes u v w

variable {α : Type u}

class seq_ty (α : Type u) :=
(data : Type v)
(destruct : data → option (α × data))

structure seq (α : Type u) : Type (max u (v+1)) :=
(pfx : list α)

digama0

/-
 - Definition of insertion sort.
 - Copyright Siva Somayyajula, 2017
 -/

namespace list

universe u
variable {α : Type u}

digama0

def zero_nhd : filter ℚ :=
lemma mem_zero_nhd {r : ℚ} (h : 0 < r) : {q | abs q < r} ∈ zero_nhd.sets :=
lemma mem_zero_nhd_le {r : ℚ} (h : 0 < r) : {q | abs q ≤ r} ∈ zero_nhd.sets :=
lemma mem_zero_nhd_iff {s : set ℚ} : s ∈ zero_nhd.sets ↔ ∃r>0, ∀q:ℚ, abs q < r → q ∈ s :=
lemma tendsto_zero_nhds {m : α → ℚ} {f : filter α} (hm : ∀r>0, {a | abs (m a) < r} ∈ f.sets) :
  tendsto m f zero_nhd :=
lemma pure_zero_le_zero_nhd : pure 0 ≤ zero_nhd :=
lemma tendsto_neg_rat_zero : tendsto has_neg.neg zero_nhd zero_nhd :=
lemma tendsto_add_rat_zero : tendsto (λp:ℚ×ℚ, p.1 + p.2) (filter.prod zero_nhd zero_nhd) zero_nhd :=
lemma tendsto_add_rat_zero' {f g : α → ℚ} {x : filter α}

digama0

import data.set.basic tactic.interactive

/-
Here's Kevin's problem:

  Let’s say I tell two of my tutees secret non-negative integers, and then I wrote
  two distinct non-negative integers on my whiteboard; one is the sum of the two
  secret integers, and the other one is not. I then take it in turns asking my
  tutees whether they know the other tutee’s number! Prove that eventually one of
  them will (truthfully) say “yes”.

digama0

import data.buffer

namespace lean_ir
/-- A simple type system based on memory representation -/
inductive type : Type
| ptr : type → type -- 4/8 bytes: pointer to data of type X
| array : type → type -- (sizeof X)*n bytes for some n: raw array of data of type X
| unit : type -- 0 bytes
| prod : type → type → type -- unboxed tuple, sizeof X + sizeof Y bytes
| bool : type -- 1 byte

digama0

import data.option data.list.basic data.int.order

attribute [derive decidable_eq] name

namespace tc

inductive level
| var : ℕ → level
| zero : level
| succ : level → level

digama0

import data.finset
open nat finset

/-- `indep E` is the type of matroids (encoded as systems of independent sets) with ground set `E` :
`finset α` -/
structure indep (α : Type*) [decidable_eq α] :=
(indep : finset (finset α))
-- (I1)
(empty_mem_indep : ∅ ∈ indep)
-- (I2)

digama0

-- presheaf of types basics and equivalence

import topology.opens topology.constructions

universes u v u₁ v₁ u₂ v₂

open topological_space

structure presheaf_of_typesU (X : Type u) [topological_space X] :=
(F : opens X → Type u)