Agda-2.3.2.2: examples/outdated-and-incorrect/cbs/Star.agda
module Star where
data Star {A : Set}(R : A -> A -> Set) : A -> A -> Set where
rf : {x : A} -> Star R x x
_<>_ : forall {x y z} -> R x y -> Star R y z -> Star R x z
module Star where
data Star {A : Set}(R : A -> A -> Set) : A -> A -> Set where
rf : {x : A} -> Star R x x
_<>_ : forall {x y z} -> R x y -> Star R y z -> Star R x z