Issues

• Incompatible Lean Version

  verse-lab/loom#28 · Filter by author Oscario0 opened on Dec 19, 2025
  8

• Missing array lemmas for grind

  verse-lab/loom#27 · Filter by author tdardinier opened on Nov 26, 2025

• Split Velvet into a separate folder

  EasyVelvet
  verse-lab/loom#26 · Filter by author volodeyka opened on Nov 21, 2025
  2

  

• Velvet and Loom logos design

  HardLoomVelvet
  verse-lab/loom#25 · Filter by author volodeyka opened on Nov 9, 2025

• Compose a Test suite for Velvet

  HardVelvet
  verse-lab/loom#24 · Filter by author volodeyka opened on Nov 9, 2025

• loom_intro tactic does not behave

  HardVelvet
  verse-lab/loom#23 · Filter by author volodeyka opened on Nov 9, 2025
  3

  

• Pretty printing for Velvet programs

  MediumVelvet
  verse-lab/loom#22 · Filter by author volodeyka opened on Nov 9, 2025

• Proof incrementality

  MediumVelvet
  verse-lab/loom#21 · Filter by author volodeyka opened on Nov 9, 2025
  7

  

• Explicit naming of annotations

  EasyVelvet
  verse-lab/loom#19 · Filter by author volodeyka opened on Nov 9, 2025