Zulip Chat Archive

Stream: general

Topic: Writing a Theory

Regivan Santiago (Feb 28 2018 at 13:57):

Dear friends, I am new in Lean and I want to write a theory. I have read logic and proof tutorial and now I want to build my own theories. I understand that they will be written in Lean Programming language. Does anyone have a simple ready theory as guide and can provide me the steps to compile it and make it available to new theories?

Sean Leather (Feb 28 2018 at 14:00):

@Regivan Santiago Have you worked through Theorem Proving in Lean?

Regivan Santiago (Feb 28 2018 at 17:34):

Not yet

Patrick Massot (Feb 28 2018 at 17:37):

You should read it. It's great.

Regivan Santiago (Feb 28 2018 at 17:51):

I will. So this is the first step.

Simon Hudon (Feb 28 2018 at 20:11):

Are you looking for help in how to make some Lean code open source and usable by others or how to structure your Lean to present a nice interface?

Last updated: Dec 20 2023 at 11:08 UTC