tests/src/infinite-loop.rs


1
2
3
4
5
6
7
8
9
10
11

//@ [coq,fstar,lean] skip
//@ [coq,fstar] aeneas-args=-use-fuel
//@ [coq,fstar] subdir=misc
// FIXME: make it work
fn bar() {}

fn foo() {
    loop {
        bar()
    }
}