News for hackers. Stuff that matters.

A comment on Show HN: Dependently typed language for proofs that you can implement in one day.

Re:Show HN: Dependently typed language for proofs that you c... by anfelor on Saturday October 02, 2021 @04:46AM (#28727101)
The Readme defines:

  // Data NonEmpty = | New a (NonEmpty a) 
  NonEmpty 
    |A :: ~ * ~> * => {(list A) :: |new}. // A list non-empty is list only with new constructor
The haskell datatype reads like a co-inductive definition: a stream of list elements. But the NonEmpty in your language should be

  data NonEmpty = New a (List a)
right?
[ Parent | on HN ]
Re:Show HN: Dependently typed language for proofs that you c... by caotic123 on Saturday October 02, 2021 @04:52AM (#28727126)
Exactly, it does not necessarily means co-data, thank you for reporting it, i will fix it.
[ Parent | on HN ]