MutuallyRecursiveTraits.lean « misc « lean « tests - aeneas - aeneas rust verifier with a hacky Isabelle backend

summary refs log tree commit diff

path: root/tests/lean/misc/MutuallyRecursiveTraits.lean

blob: b0fcb9e95f1e2787c167d87387a6c3614ce63779 (plain)

-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [mutually_recursive_traits]
import Base
open Primitives

namespace mutually_recursive_traits