Code

feat: rename request handler#2462

Code

Merged

mhuisi merged 3 commits intoleanprover:masterleanprover/lean4:masterfrom digama0:renamedigama0/lean4:renameCopy head branch name to clipboardNov 21, 2023

+152-26

Commits

Commits on Nov 16, 2023

• feat: rename request handler

  digama0

  committed
  0472414

  Copy full SHA for 0472414

• fix: RefInfo for structure ctor

  digama0

  committed
  38494c7

  Copy full SHA for 38494c7

Commits on Nov 20, 2023

• chore: review fixes

  digama0

  committed
  c4b56e8

  Copy full SHA for c4b56e8