Repository navigation

v2 infer: application-argument inhabitance before admission - #11296

Merged

briansrls merged 30 commits into

mainfrom

session/fierce-swift-182

Sep 14, 2026

Merged

v2 infer: application-argument inhabitance before admission#11296
briansrls merged 30 commits into
mainfrom
session/fierce-swift-182

Commits on Sep 13, 2026
- Give v2 infer an application-argument inhabitance judgment.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  0e8067b
- Merge origin/main into session/fierce-swift-182.
  gunbc-ci-auto-heal
  committed
  e66e737
- Consume find_witness for inhabitance; keep Undecidable as a counted frontier.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  f9b823b
- Treat unjudgeable inhabitance as counted Undecidable, not refusal.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  09e0e6e
- State the inhabitance rung as a decidable refusal plus counted unjudgeable applications.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  21219db
- Make inhabitance constructors resolve as a coproduct, not an alias.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  1bc4017
- Quarantine inhabitance commentary and drop unused inhabitance surface.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  f756ead
- Advance inhabitance zip remaining with list_tail.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  e7673e9
- Match inhabitance undecidable connectives by coproduct arm.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  49e1d66
- Consume DeclaredTypeObligation fields in the refusal diagnostic.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  ab7097b
- Match InhabitanceVerdict by arm in infer, not double-Absent.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  43d5d61
- Look up operator Arrow declarations with fold_node.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  c9bdf3c
- Return inhabitance refusal reasons as Symbol from both if arms.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  b1ba8df
- Require a unique operator Arrow; zip formals with zip_map.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  204c46f
- Cover childless Transforms on the inhabitance row.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  9d696d2
- Merge Arrow-declaration lists outside the NodeFold step.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  cf10fae
- Refuse decidable positional arity mismatch.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  ecb2a40
Commits on Sep 14, 2026
- Judge inhabitance only on an inline Arrow operator.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  7409d47
- State why inhabitance does not consume coercion_fold.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  baf6faf
- Attach inhabitance commentary to functions, not type coproducts.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  1b1cad8
- State that application inhabitance is exact structural equality.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  88e367a
- Classify Cardinality formals on the infer gather fold.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  d148047
- Call the inhabitance undecidable classifier from infer.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  5f06ce5
- Build optional-carrier specimens in v2.std.inhabitance.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  d71c1e5
- Put inhabitance rung facts in a recurring-failure-mode row.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  dbeebc7
- Escape the RFM receipt so `{declared}` is not interpolation.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  073086d
- Treat TypeNode Cardinality as Bounded, like Instantiation.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  dd06ae3
- Keep Cardinality multiplicity; record unproven descent on facts.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  82e8fcd
- Restore Cardinality descent refuse on infer.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  d07563a
- Name the infer Outcome reason the optional-formal RED actually sees.
  
  gunbc-ci-auto-heal
  and
  cursoragent
  committed
  f947b6b

Commits

Commits on Sep 13, 2026

Commits on Sep 14, 2026