Code

For loops#954

Code

Merged

Chris-Hawblitzel merged 21 commits intomainverus-lang/verus:mainfrom for-loopverus-lang/verus:for-loopCopy head branch name to clipboardJan 24, 2024

+1,553-383

Commits

Commits on Dec 12, 2023

• In lifetime_generate, only select from all_impls(trait_id) on demand

  Chris-Hawblitzel

  committed
  0b8ce08

  Copy full SHA for 0b8ce08

Commits on Dec 13, 2023

• Support into_iter for Range

  Chris-Hawblitzel

  committed
  bda76f8

  Copy full SHA for bda76f8

• Mark feature(step_trait) as cfg_attr(verus_keep_ghost)

  Chris-Hawblitzel

  committed
  d1085d2

  Copy full SHA for d1085d2

Commits on Jan 3, 2024

• Initial support for for-loops

  Chris-Hawblitzel

  committed
  65847ae

  Copy full SHA for 65847ae

Commits on Jan 5, 2024

• For for-loops, keep ghost iterator separate from exec iterator

  Chris-Hawblitzel

  committed
  5b89140

  Copy full SHA for 5b89140

• Refactor syntax macro visit order on loop invariants

  Chris-Hawblitzel

  committed
  31cd01f

  Copy full SHA for 31cd01f

• Switch some parse_quote_spanned to Verbatim quote_spanned

  Chris-Hawblitzel

  committed
  01bac5f

  Copy full SHA for 01bac5f

• Add Vec custom iterator example

  Chris-Hawblitzel

  committed
  7187d6b

  Copy full SHA for 7187d6b

Commits on Jan 9, 2024

• Remove old ignored test

  Chris-Hawblitzel

  committed
  6d66cc1

  Copy full SHA for 6d66cc1

• Rewrite InferSpecForLoopIter in modes not in ast_simplify

  Chris-Hawblitzel

  committed
  7a36030

  Copy full SHA for 7a36030

• Push/pop modes.rs state around InferSpecForLoopIter

  Chris-Hawblitzel

  committed
  8e0b755

  Copy full SHA for 8e0b755

Commits on Jan 10, 2024

• Limit axiom_spec_range_next to specific types

  Chris-Hawblitzel

  committed
  635e34c

  Copy full SHA for 635e34c

• Replace ghost_condition with ghost_ensures

  Chris-Hawblitzel

  committed
  f6ab69e

  Copy full SHA for f6ab69e

Commits on Jan 11, 2024

• Merge branch 'main' into for-loop

  Chris-Hawblitzel

  committed
  f12572c

  Copy full SHA for f12572c

• Add ret_mode to TypingSnapshot

  Chris-Hawblitzel

  committed
  569b870

  Copy full SHA for 569b870

• Fix comment and panic message

  Chris-Hawblitzel

  committed
  5b2a059

  Copy full SHA for 5b2a059

Commits on Jan 17, 2024

• Return Option from ghost_peek_next and ghost_decrease

  Chris-Hawblitzel

  committed
  b602bfe

  Copy full SHA for b602bfe

• Update loops.rs test with more precise ghost_peek_next

  Chris-Hawblitzel

  committed
  7393ae1

  Copy full SHA for 7393ae1

Commits on Jan 20, 2024

• Match for loop translation from https://doc.rust-lang.org/reference/expressions/loop-expr.html

  Chris-Hawblitzel

  committed
  1fe732a

  Copy full SHA for 1fe732a

Commits on Jan 24, 2024

• Refactor state in modes.rs (#961)

  Show description for e062d0a
  Chris-Hawblitzel

  authored
  e062d0a

  Copy full SHA for e062d0a

• Merge branch 'main' into for-loop

  Chris-Hawblitzel

  committed
  7aa5217

  Copy full SHA for 7aa5217