can't label assumptions

[kjx]

Summary

assume FOO: x == 4; //doesn't work

Background and Motivation

doing something to complex and wrongly

Proposed Feature

being able to label assumptions in exactly the same was assertions are labelled...

Alternatives

other options:

• wrap assumption in a labelled assertion

assert FOO: forall x <- m.Keys, oo <- x.AMFO :: (m[oo] in m[x].AMFO) //proved ibn forall/ensuring
  by { assume forall x <- m.Keys, oo <- x.AMFO :: (m[oo] in m[x].AMFO);  }

• restructure everyting
• switch to IDRIS
• switch to Coq
• switch to lean