From 485abe7a1016b5bdcadfcf8a379947aefd849236 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Mar 2019 13:10:33 -0700 Subject: [PATCH] chore(library/init/core): we can parse `core.lean` @kha --- library/init/core.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index f777d07c9c..8122562403 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -296,7 +296,7 @@ structure Subtype {α : Sort u} (p : α → Prop) := inductive Exists {α : Sort u} (p : α → Prop) : Prop | intro (w : α) (h : p w) : Exists -attribute [ppUsingAnonymousConstructor] Sigma Psigma Subtype Pprod and +attribute [ppAnonymousCtor] Sigma Psigma Subtype Pprod and class inductive Decidable (p : Prop) | isFalse (h : ¬p) : Decidable @@ -1392,7 +1392,7 @@ end Plift /- pointed types -/ structure PointedType := -(Type : Type u) (val : Type) +(type : Type u) (val : type) /- Inhabited -/ @@ -1420,7 +1420,7 @@ instance : Inhabited True := ⟨trivial⟩ instance : Inhabited Nat := ⟨0⟩ -instance : Inhabited PointedType := ⟨{Type := Punit, val := ⟨⟩}⟩ +instance : Inhabited PointedType := ⟨{type := Punit, val := ⟨⟩}⟩ class inductive nonempty (α : Sort u) : Prop | intro (val : α) : nonempty