Code

minor updates#121

Code

Merged

yangky11 merged 3 commits intomainlean-dojo/LeanDojo:mainfrom devlean-dojo/LeanDojo:devCopy head branch name to clipboardJan 2, 2024

+4-12

Commits

Commits on Dec 20, 2023

• minor edits

  

  Kaiyu Yang

  committed
  9afa304

  Copy full SHA for 9afa304

• Merge branch 'dev' of github.com:lean-dojo/LeanDojo into dev

  

  Kaiyu Yang

  committed
  2dc0759

  Copy full SHA for 2dc0759

• bump

  

  Kaiyu Yang

  committed
  0400d85

  Copy full SHA for 0400d85