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 https://github.com/future-proof-iot/RIOT-rs/pull/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.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[maximebuyse]

This is because of #888