[Agda] Re: Inheriting fields
N. Raghavendra
raghu at hri.res.in
Thu Feb 12 19:27:11 CET 2015
At 2015-02-12T15:30:47+01:00, Andreas Abel wrote:
> record fields can be omitted if type inference reconstructs them
> through unification. In this case, the values of Carrien and
> _\approx_ are determined by the type of isEquivalence, so the unifier
> puts them in.
Ok. Carrier and _≈_ are the parameters of isEquivalence, so specifying
isEquivalence is enough to specify all the fields of setoid.
Thanks and cheers,
Raghu.
--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/
More information about the Agda
mailing list