> Il giorno 27 ott 2017, alle ore 17:35, Chun Tian <binghe.l...@gmail.com> ha > scritto: > > Thanks for your comments. > > If I quotient [1] the original CCS datatype into another one, I could expect > to have the a “fix” constructor with a finite map, right? > > On the the other side, what if I directly define another similar constant, > say “Fix” in this form: > > |- Fix fm X = fix (alist_to_fmap ls) X
Sorry, it should be: |- Fix fm X = fix (fmap_to_alist fm) X > > And in all theorems I only use “Fix”. Is this possible (as a cheap solution) > for resolving the “structural congruences” issue? > > Regards, > > Chun Tian > > [1] Homeier, P.V.: Higher Order Quotients in Higher Order Logic. preparation; > draft available at http://www cis …. (1969).
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
