view paper/src/Equiv.agda.replaced @ 4:b5fffa8ae875

fix chapter hoare
author ryokka
date Wed, 29 Jan 2020 22:36:17 +0900
parents c7acb9211784
children
line wrap: on
line source

data _@$\equiv$@_ {a} {A : Set a} (x : A) : A @$\rightarrow$@ Set a where
  refl : x @$\equiv$@ x