Zulip Chat Archive
Stream: lean4
Topic: where is the lean4 core library defined?
Julian Berman (Oct 14 2022 at 23:18):
Specifically https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L1015
Gabriel Ebner (Oct 14 2022 at 23:18):
The file is called Prelude.lean (with an uppercase P). See also https://github.com/leanprover/vscode-lean4/issues/254
Arien Malec (Oct 14 2022 at 23:33):
Got it, & in the raw source, it's under /src/Init
Last updated: May 02 2025 at 03:31 UTC