Closed eupp closed 2 years ago
make lposet morphisms class instances opaque (in order to hide large proof terms), but leave Pack instances transparent (in order to allow unfolding)
use sub_ffun to define finite versions of morphisms
sub_ffun
add inh notations and lemmas --- ?|T| for inhabited, ??|T| for decidable check of inhabitance (for finite types).
inh
?|T|
??|T|
rename Bij --> bHom
Bij
bHom
add type of injective homomorphism iHom
iHom
make lposet morphisms class instances opaque (in order to hide large proof terms), but leave Pack instances transparent (in order to allow unfolding)
use
sub_ffunto define finite versions of morphismsadd
inhnotations and lemmas ---?|T|for inhabited,??|T|for decidable check of inhabitance (for finite types).rename
Bij-->bHomadd type of injective homomorphism
iHom