HigherOrderCO / Kind

A modern proof language
https://higherorderco.com
MIT License
3.55k stars 141 forks source link

Syntax in the explanation #585

Open iacore opened 3 weeks ago

iacore commented 3 weeks ago

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?