blob: b1758acc02cca75092bfaa6d148ad8f5c857c578 (
plain)
1
2
3
4
5
6
7
8
|
// RUN: %boogie -noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
type Seq T;
function Seq#Length<T>(Seq T) returns (int);
function Seq#Empty<T>() returns (Seq T);
axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);
|