search

leanprover / LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Apache License 2.0
60 stars 16 forks source link

chore: clean up unused arguments #53

Closed semorrison closed 1 year ago

semorrison commented 1 year ago

Description

These spurious unused arguments will later cause warnings as we start bumping the toolchain, so let's get them out of the way now.