/tests/lean/misc/
../
MutuallyRecursiveTraits.lean