Why named vs implicit arguments in function declarations?

Stream: new members

[Castedo Ellerman]

Learning from textbook Logic and Mechanized Reasoning I read

inductive Lit where
  | tr  : Lit
  | fls : Lit
  | pos : String → Lit
  | neg : String → Lit

inductive NnfForm where
  | lit  (l : Lit) : NnfForm
...

Why not

  | neg (s : String): Lit

or

  | lit : Lit → NnfForm

?

Is it just a subjective judgement call whether a named argument makes it easier to read (and error messages realted to it)? Am I using the terms "named argument" and "implicit argument" correctly?

[Eric Wieser]

"implicit argument" means {s : String}, I think probably "anonymous" is a better name for what you mean

[Moritz R]

I can only answer from the perspective of the code actions that generate match and induction cases. These will try to use the names (like s) supplied in the definiton.

[Moritz R]

These Codeactions are in Batteries (and by import of Batteries, also in mathlib)

[Moritz R]

e.g.

[Moritz R]

import Batteries
inductive Lit where
  | tr  : Lit
  | fls : Lit
  | pos (s : String) : Lit
  | neg : String → Lit
def bla (t : Lit) :=
  match t with -- put your cursor directly after `with`, click the lightbulb (or the corresponding vscode-shortcut) and generate the patterns.

[Moritz R]

gives

[Moritz R]

import Batteries
inductive Lit where
  | tr  : Lit
  | fls : Lit
  | pos (s : String) : Lit
  | neg : String → Lit

def bla (t : Lit) :=
  match t with
  | .tr => _
  | .fls => _
  | .pos s => _
  | .neg _ => _ -- put your cursor directly after `with`, click the lightbulb (or the corresponding vscode-shortcut) and generate the patterns.

[Moritz R]

Notice the s at .pos and the _ at .neg

[Moritz R]

So for arguments that should have a standard name when doing induction/match, i would say give them a name