346_unused_warning_8.mlw 228 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
use int.Int

exception E
exception F
exception G
exception H

val f (x: int) : int
    ensures { x = 42       }
    raises  { F -> x = -42 }
    raises  { E -> x <> x  }
    raises  { G -> x = x   }
    raises  { H -> false   }