Here is something that I think used to work in Lean 3, although I no longer have a working installation of Lean 3 with which to check that the details of this minimal example are precisely correct. I could define a function f like this:

section A

variable (x : Nat)
include x

def f (y : Nat) : Nat := y

end A

#check f

Because of the directive include x, the function f would actually have two arguments x and y, with x being present but unused. In other words, the type would be Nat -> Nat -> Nat.

This does not work in Lean 4: the line include x produces an error message unexpected identifier; expected command. Because the word "include" is used in so many different contexts, it is hard to search for information about this. Can anyone let me know whether there is a new syntax for this feature or whether it has been dropped?


1 Answer 1


I believe include annd omit are still missing. There is some discussion, which you can read at the below links, about a possible better alternative include … in and omit … in, but those have not been implemented yet that I’m aware.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.