PROJECT_LANG_1.lean

#print "\n" -- Start of script
#print "Project language file 1"
#print "For: seanpm2001/Learn-Lean"
#print "About: "
#print "I decided to make Lean the main project language file for this project (Seanpm2001/Learn-Lean) as Lean is the language this project is dedicated to, because this project is about learning the Lean programming language. It only makes sense to Lean the official language for this project. It is getting its own project language file, starting here."
#print "\n" -- Output
#print "\n" -- Project language file 1
#print "\n" -- For: seanpm2001/Learn-Lean
#print "\n" -- About:
#print "\n" -- I decided to make Lean the main project language file for this project (Seanpm2001/Learn-Lean) as Lean is the language this project is dedicated to, because this project is about learning the Lean programming language. It only makes sense to Lean the official language for this project. It is getting its own project language file, starting here.
#print "\n" -- File info
#print "\n" -- File type: Lean source file (*.lean)
#print "\n" -- File version: 1 (2022, Sunday, September 18th at 5:34 pm PST)
#print "\n" -- Line count (including blank lines and compiler line): 16
#print "\n" -- End of script