Zulip Chat Archive

Stream: general

Topic: Writing a Theory


view this post on Zulip 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?

view this post on Zulip Sean Leather (Feb 28 2018 at 14:00):

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

view this post on Zulip Regivan Santiago (Feb 28 2018 at 17:34):

Not yet

view this post on Zulip Patrick Massot (Feb 28 2018 at 17:37):

You should read it. It's great.

view this post on Zulip Regivan Santiago (Feb 28 2018 at 17:51):

I will. So this is the first step.

view this post on Zulip 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: May 11 2021 at 12:15 UTC