Repository navigation

Origin note: say what a call's return refinement guarantees about an argument it gives - #530

Merged

CatarinaGamboa merged 7 commits into

mainfrom

Nov 11, 2026

Merged

Origin note: say what a call's return refinement guarantees about an argument it gives#530
CatarinaGamboa merged 7 commits into
mainfrom
from-note-f4

Commits on Nov 11, 2026
- Say what a call's return refinement guarantees about an argument it gives
  
  CatarinaGamboa
  and
  claude
  committed
  563dfb6
- Drop a ghost definition only when nothing else constrains that ghost
  
  CatarinaGamboa
  and
  claude
  committed
  4c1890c
- Keep a ghost definition when the ghost is applied anywhere else
  
  CatarinaGamboa
  and
  claude
  committed
  9d2d9e7
- Keep a ghost definition when an alias may apply the ghost
  
  CatarinaGamboa
  and
  claude
  committed
  edaba46
- Never take a built-in function for a ghost of the same name
  
  CatarinaGamboa
  and
  claude
  committed
  b7df716
- Write the returned-value note as Origin: <File>:<line>, <call> guarantees ...
  
  CatarinaGamboa
  and
  claude
  committed
  7b0cf52
- Leave out the returned-value note when it names an argument by its parameter
  
  CatarinaGamboa
  and
  claude
  committed
  fa84640