max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/core): we can parse core.lean

Browse source 
@kha
This commit is contained in:
Leonardo de Moura 2019-03-20 13:10:33 -07:00
parent e0b0ca4830
commit 485abe7a10
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/core.lean
View file

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