this is a) incomplete, and b) imprecise, given that there's no notion of a carrier set, we just assume it to be int for now, and i haven't settled on the right language to describe the existence of a partial inverse.
anyway, it works for the definition of Nat which i think is a good enough starting point
This file has not been changed.
This file has not been changed.
This file has not been changed.
This file has not been changed.
This file has not been changed.
This file has not been changed.
This file has not been changed.
This file has not been changed.
This file has not been changed.
This file has not been changed.
This file has not been changed.
this is a) incomplete, and b) imprecise, given that
there's no notion of a carrier set, we just assume it to be
int for now, and i haven't settled on the right language
to describe the existence of a partial inverse.
anyway, it works for the definition of Nat which i think is a good
enough starting point
this is a) incomplete, and b) imprecise, given that
there's no notion of a carrier set, we just assume it to be
int for now, and i haven't settled on the right language
to describe the existence of a partial inverse.
anyway, it works for the definition of Nat which i think is a good
enough starting point
this is a) incomplete, and b) imprecise, given that
there's no notion of a carrier set, we just assume it to be
int for now, and i haven't settled on the right language
to describe the existence of a partial inverse.
anyway, it works for the definition of Nat which i think is a good
enough starting point