Hi,
I have a question,
What tactic I should use to solve this problem?
!s0. flipslv (flipslv (Next s0 x)) = Next s0 x
----------------------------------------------
x. flipslv (flipslv x) = x
The flipslv function is just simply reverses x which is a slv datatype.
The datatype declaration is written as bellow:
val _ = Hol_datatype`
slv = Single of stdl
| Next of stdl => slv
`;
And I also have this definitions before:
val flipnext_def = Define `(flipnext (Next a b) c = flipnext b (Next a
c))
/\ (flipnext (Single a) c = Next a c)`;
val flipslv_def = Define `(flipslv (Next a b) = flipnext b (Single a))
/\ (flipslv (Single a) = (Single a))`;
I think the pattern has matched (by replace "x" with "Next s0 x"), but I
don't know how to do. Could anyone help me?
Thank you.
--
Dwi Teguh Priyantini
Fasilkom UI - 1506782322
------------------------------------------------------------------------------
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
