Closed c-cube closed 8 years ago
spec head : pi a. list a -> a and tail : pi a. list a -> list a := <axioms> instead of separate declarations.
spec head : pi a. list a -> a and tail : pi a. list a -> list a := <axioms>
Should only have to modify parser + type inference.
fixed by 8ed57d8
c-cube
commented
8 years ago c-cube
commented
8 years ago
spec head : pi a. list a -> a and tail : pi a. list a -> list a := <axioms>instead of separate declarations.Should only have to modify parser + type inference.