ConDai

CoInductive CoNat :=
| CoZ : CoNat
| CoS : CoNat -> CoNat.

CoInductive bisimilar : CoNat -> CoNat -> Prop :=
| bisimilar_CoZ: bisimilar CoZ CoZ
| bisimilar_CoS: forall n m, bisimilar m n ->  bisimilar (CoS m) (CoS n).


Definition evalCoNat (n : CoNat) :=

ConDai

module Channel {

  use semaphore;

  record chan {
    type eltType;
    var size:   int;
    var buffer: [0..size-1] eltType;
    
    var full: semaphore.Semaphore;