solve mixin dependencies via TC#596

Open

gares wants to merge 9 commits into

math-comp:masterfrom

Tragicus:mixin-tc

Commits on Jun 4, 2026

wip
Tragicus
committed
wip
Tragicus
committed

Commits on Jun 5, 2026

use projection instead of unification to extract the mixin from the class
Tragicus
committed
Revert "use projection instead of unification to extract the mixin from the class"
Tragicus
committed

Commits on Jun 8, 2026

fix Build notation, Build implicits, instance elaboration and clause accumulation
Tragicus
committed
add alias for Axioms_ with different implicits
Tragicus
committed

Commits on Jun 12, 2026

Commits on Jun 17, 2026

declare mixin instances only for the first class
Tragicus
committed