[downstream PR] Julia's instance check - #14536

Draft

datokrat wants to merge 16 commits into

leanprover:paul/nightly-2026-08-16-testfrom

datokrat:julias-instance-check

Commits on Aug 17, 2026

experiment: always check types for instance metavariables at instances transparency

TwoFX
authored and
datokrat
committed
561d42c
fixes

TwoFX
authored and
datokrat
committed
020bb06
Introduct option

TwoFX
authored and
datokrat
committed
e1bde31
experiment: do not bump transparency when assigning `outParam`s

TwoFX
authored and
datokrat
committed
11206ad
experiment: fix `inferInstanceAs` elaborator

TwoFX
authored and
datokrat
committed
4200b4b
fixes for stage2
datokrat
committed
8e04897
mark-or-synth strategy
datokrat
committed
a2d3c7b
synthetic auxMVars
datokrat
committed
0ef0c69
clean up Lean.Environment
datokrat
committed
bbc4f82

Commits on Aug 18, 2026

respectTransparency.outParams disabled by default; respectTransparency.instances enabled even if respectTransparency.types is disabled
datokrat
committed
cc7922e

Commits on Aug 20, 2026

instance linter
datokrat
committed
7dd284a
simp-splitting warnings
datokrat
committed
275bacf

Commits on Aug 21, 2026

feat: check instance arguments after definitional rewrites

datokrat
and
claude
committed
309e9b8
feat: add `@[lax_instance_defeq]` to exempt classes from the strict instance check

datokrat
and
claude
committed
4b6ada0
chore: disable `dsimp.resynthInstances` by default on this branch

datokrat
and
claude
committed
07ce7d7

Commits on Aug 28, 2026

poke
datokrat
committed
983d39e