lean4-htt/tests/pkg/mod_clash/depB/Diff.lean at master - max/lean4-htt - maxgit: wireguard access, git repository.

max/lean4-htt

Mac Malone 687698e79d

test: module clash across packages (#11246 )

This PR adds a test that covers importing modules defined in multiple
packages.

Currently, will resolve the module to its first occurrence in the its
search order. However, this will soon change, so this test is designed
to analyze that behavior.

2025-11-19 02:23:34 +00:00

1 line

18 B

Text

Raw Permalink Blame History

def bar := "depB"