Code

Support for ensures in spec fns#744

Code

Draft

jonhnet wants to merge 4 commits intomainverus-lang/verus:mainfrom jonh-spec-ensuresverus-lang/verus:jonh-spec-ensuresCopy head branch name to clipboard

+474-150

Commits

Commits on Aug 9, 2023

• very rough draft with andrea; can't yet prove ensures

  

  Jon Howell

  committed
  bb9fe60

  Copy full SHA for bb9fe60

Commits on Aug 12, 2023

• progress building spec fn ensures with chris

  

  Jon Howell

  committed
  8eb72f4

  Copy full SHA for 8eb72f4

Commits on Aug 13, 2023

• express current progress as tests, future goals as ignored tests

  

  Jon Howell

  committed
  3aef40f

  Copy full SHA for 3aef40f

• tidy up

  

  Jon Howell

  committed
  3573511

  Copy full SHA for 3573511