[Liberty-eiffel] locals in postcondition

[Raphael Mack]

Hello all,

is it allowed to access locals in a postcondition? I don't think it  
makes much sense...
If we have a closure in the postcondition we get warnings about using  
the same variable names:

   add_instructions (a_instructions: TRAVERSABLE[INSTRUCTION])
      local
         i: INTEGER
      do
         i := 3
      ensure
         added_last_in_reverse_order: (create {ZIP[INSTRUCTION,  
INTEGER]}.make(a_instructions,
                                                                       
         1 |..| a_instructions.count)
                                       ).for_all(agent (inst:  
INSTRUCTION; i: INTEGER): BOOLEAN
                                                 do
                                                    Result := inst =  
instructions_list.item(instructions_list.upper - i + 1)
                                                 end)
      end

is this what we want?

Rapha