fact: Definition for_ (anno:LOOP_ANNOTATION.t) (init:list STATEMENT.t) (test:Expression) (step:list Expression) (body:STATEMENT.t) := ForLoop (Block := BLOCK.t) anno init test step body.
imports: Coq(List) JML(ListHelpers) JML(JMLExpressionNotations) JML(JMLProgramPlusImpl)