Code

feat: use captureStr#2

Code

Open

fgdorais wants to merge 6 commits intoJamesGallicchio:mainJamesGallicchio/http:mainfrom fgdorais:capturefgdorais/http:captureCopy head branch name to clipboard

+101-83

Commits

Commits on Dec 22, 2023

• chore: update lean toolchain

  fgdorais

  committed
  5c96cde

  Copy full SHA for 5c96cde

• fix: use Parser.Char.captureString

  fgdorais

  committed
  7179376

  Copy full SHA for 7179376

Commits on Dec 23, 2023

• Add CI

  

  JamesGallicchio

  authored and

  fgdorais

  committed
  cf6178a

  Copy full SHA for cf6178a

• fix: no mathlib cache :)

  

  JamesGallicchio

  authored and

  fgdorais

  committed
  ec2b0a2

  Copy full SHA for ec2b0a2

• chore: cleanup old eval

  

  JamesGallicchio

  authored and

  fgdorais

  committed
  077c8aa

  Copy full SHA for 077c8aa

• fix: new capture functions

  fgdorais

  committed
  2504735

  Copy full SHA for 2504735