What is meant by #hol?
Posted: Thu Apr 20, 2023 10:17 am
Can someone help me and tell me what #hol means please?
#hol is the main HOL channel/chatroom on the IRC chat network. It's explained in lesson 1 of HOL 101 in the section called 'IRC (HOL Chat') and you can find instructions for accessing it in assignment 1 under the section called 'IRC'. There's more information in the handbook but that's more complex and probably has more detail than you need.
Please let us know if you need anything explaining a little more.
