--import super namespace demo variables (a b : Prop) example : a → b → a := λ ha hb, ha /- Church encoding def and (a b : Prop) : Prop := ∀ C : Prop, (a → b → C) → C lemma and.intro (ha : a) (hb : b) : and a b := λ C f, f ha hb lemma and.left (h : and a b) : a := h a (λ ha hb, ha)-/ inductive and | intro : a → b → and #check and.intro --#check and.cases_on example : and a b → and b a --| (and.intro ha hb) := and.intro hb ha | ⟨ha, hb⟩ := ⟨hb, ha⟩ inductive or | inl {} : a → or | inr {} : b → or example : or a b → or b a | (or.inl ha) := or.inr ha | (or.inr hb) := or.inl hb inductive true | intro : true inductive false' example : false' → a. def not' := a → false' #check not lemma foo : (¬a → b) → (¬b → a) := assume : ¬a → b, assume : ¬b, show a, from classical.by_contradiction $ assume : ¬a, have b, from ‹¬a → b› this, show false, from ‹¬b› this lemma foo' : (¬a → b) → (¬b → a) := by intros; apply classical.by_contradiction; simp * at * --by super variable α : Type example (p q : α → Prop) : (Π x, p x) ∧ (Π x, q x) → Π x, p x ∧ q x := assume ⟨hp, hq⟩, assume x, ⟨hp x, hq x⟩ inductive ex' {α : Type} (p : α → Prop) | intro : Π x, p x → ex' example (p : α → α → Prop) : (∃ x, ∀ y, p x y) → ∀ y, ∃ x, p x y := assume ⟨x, hx⟩, assume y, ⟨x, hx y⟩ inductive eq' {α : Type} : α → α → Prop | refl : Π x : α, eq' x x /-inductive magma (α : Type) | mk : Π (op : α → α → α) (carrier : set α) (closed : Π {x y : α}, x ∈ carrier → y ∈ carrier → op x y ∈ carrier), magma-/ structure magma (α : Type) := (op : α → α → α) (carrier : set α) (closed : Π {x y : α}, x ∈ carrier → y ∈ carrier → op x y ∈ carrier) #check magma.op def nat.magma : magma ℕ := { op := (+), carrier := set.univ, closed := by intros; trivial } def nat3.magma : magma ℕ := { op := λ n m, (n + m) % 3, carrier := {0, 1, 2}, closed := by intros; cases_matching* [set.mem _ _, has_mem.mem _ _]; simp *; repeat { apply _root_.or.inl rfl <|> apply _root_.or.inr } } lemma magma.closed3 (x : α) (m : magma α) : x ∈ m.carrier → m.op x (m.op x x) ∈ m.carrier := λ h, m.closed h (m.closed h h) end demo