-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [infinite_loop]
import Base
open Primitives
set_option linter.dupNamespace false
set_option linter.hashCommand false
set_option linter.unusedVariables false

namespace infinite_loop

/- [infinite_loop::bar]:
   Source: 'tests/src/infinite-loop.rs', lines 4:0-4:8 -/
def bar : Result Unit :=
  Result.ok ()

/- [infinite_loop::foo]: loop 0:
   Source: 'tests/src/infinite-loop.rs', lines 6:0-10:1 -/
divergent def foo_loop : Result Unit :=
  do
  let _ ← bar
  foo_loop

/- [infinite_loop::foo]:
   Source: 'tests/src/infinite-loop.rs', lines 6:0-6:8 -/
@[reducible] def foo : Result Unit :=
               foo_loop

end infinite_loop