search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.75k stars 427 forks source link

unused variable FP with forall syntax in signature #6201

Open digama0 opened 4 days ago

digama0 commented 4 days ago 
axiom Foo : ∀ (a : Nat), Prop
            -- ^ unused variable `a`

This warning does not happen when using the syntax axiom Foo : (a : Nat) → Prop. (This is supposed to be an exception to the usual unused variable rules because it is a function signature variable, visible in the docstring and also accessible via the Foo (a := 0) syntax.)

Occurs on latest nightly (leanprover/lean4:nightly-2024-11-24).