Supporting the Iterator trait

[ROMemories]

hax does not currently seem to support the Iterator trait in F*, when manually implementing it.
For instance, the following does get extracted to F*, but does not lax check:

struct Foo;

impl Iterator for Foo {
    type Item = ();

    fn next(&mut self) -> Option<Self::Item> {
        None
    }
}

view in hax playground

Lax checking currently outputs the following:

* Error 72 at Playground.fst(9,36-9,46):
  - Identifier not found: [Core.Iter.Traits.Iterator.t_Iterator]
  - Module Core.Iter.Traits.Iterator resolved into Core.Iter.Traits.Iterator,
    definition t_Iterator not found

cc future-proof-iot/RIOT-rs#460

[W95Psp]

Thanks for the bug report!
Things are indeed a bit rough on the edges around iterators.

We won't have time this week to take a look, but we will try to find an answer next week.