Code

feat: add --include-lean option#25

Code

Merged

kim-em merged 4 commits intomainleanprover-community/import-graph:mainfrom include-leanleanprover-community/import-graph:include-leanCopy head branch name to clipboardAug 30, 2024

+13-5

Commits

Commits on Aug 29, 2024

• feat: add --include-lean option

  kim-em

  committed
  4210520

  Copy full SHA for 4210520

• handle Init and Std

  kim-em

  committed
  97c056c

  Copy full SHA for 97c056c

• better logic

  kim-em

  committed
  d8b01ef

  Copy full SHA for d8b01ef

Commits on Aug 30, 2024

• Update Main.lean

  Show description for 3347220
  

  kim-em

  and

  joneugster

  authored
  3347220

  Copy full SHA for 3347220