// RUN: %dafny "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

type MyType  // compile error: opaque type
iterator Iter()  // compile error: body-less iterator
ghost method M()  // compile error: body-less ghost method
method P()  // compile error: body-less method
method Q()
{
  if g == 0 {
    assume true;  // compile error: assume
  }
}
ghost var g: int;

function F(): int  // compile error: body-less ghost function
function method H(): int  // compile error: body-less function method

lemma Lemma() {
  assume false;  // compile error: assume
}
ghost method GMethod() {
  assume false;  // compile error: assume
}

function MyFunction(): int
{
  assume false;  // compile error: assume
  6
}

function MyCalcFunction(): int
{
  calc <= {
    2;
    6;
    { assume true; }  // compile error: assume
    10;
  }
  12
}