-
Notifications
You must be signed in to change notification settings - Fork 146
Open
Description
I was reading https://github.com/HigherOrderCO/Kind1/blob/master/blog/1-beyond-inductive-datatypes.md, and there's one part I don't quite understand.
// Natural numbers
Nat: Type
self(P: Nat -> Type) ->
(zero: P(Nat.zero)) ->
(succ: (pred: Nat) -> P(Nat.succ(pred))) ->
P(self)
If it's like the code below, it makes sense to me.
// Natural numbers
Nat: Type
(self : Nat) ->
(P: Nat -> Type) ->
(zero: P(Nat.zero)) ->
(succ: (pred: Nat) -> P(Nat.succ(pred))) ->
P(self)
So what is self
?
Metadata
Metadata
Assignees
Labels
No labels