Mercurial > urweb
comparison src/corify.sml @ 251:326fb4686f60
Monoize transaction identifiers; improve disjointness prover on irreducible folds; change 'query' type
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 31 Aug 2008 10:36:54 -0400 |
parents | b6b75e6e0898 |
children | 42dfb0d61cf0 |
comparison
equal
deleted
inserted
replaced
250:98f551ddd54b | 251:326fb4686f60 |
---|---|
815 ran), loc) | 815 ran), loc) |
816 val e = (L.EModProj (m, ms, s), loc) | 816 val e = (L.EModProj (m, ms, s), loc) |
817 | 817 |
818 val ef = (L.EModProj (basis, [], "bind"), loc) | 818 val ef = (L.EModProj (basis, [], "bind"), loc) |
819 val ef = (L.ECApp (ef, ran'), loc) | 819 val ef = (L.ECApp (ef, ran'), loc) |
820 val ef = (L.ECApp (ef, ran), loc) | |
820 val ef = (L.EApp (ef, (L.EApp (e, (L.ERel 0, loc)), loc)), loc) | 821 val ef = (L.EApp (ef, (L.EApp (e, (L.ERel 0, loc)), loc)), loc) |
821 | 822 |
822 val eat = (L.CApp ((L.CModProj (basis, [], "transaction"), loc), | 823 val eat = (L.CApp ((L.CModProj (basis, [], "transaction"), loc), |
823 ran), loc) | 824 ran), loc) |
824 val ea = (L.EAbs ("p", ran', eat, | 825 val ea = (L.EAbs ("p", ran', eat, |