Zulip Chat Archive

Stream: general

Topic: Lean trusted base

Karl Palmskog (Jan 12 2019 at 03:35):

Does anyone know if there is a breakdown of the Lean trusted base somewhere? As in, "to trust your Lean code/proofs, you have to accept ...", which is done for Coq in its wiki: https://github.com/coq/coq/wiki/Presentation#what-do-i-have-to-trust-when-i-see-a-proof-checked-by-coq

And is there anything similar to the Coq Print Assumptions <name>. command (https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.print-assumptions) in Lean?

Bryan Gin-ge Chen (Jan 12 2019 at 04:11):

I'm sure others are more knowledgeable than me, but for the first question you might be interested in @Mario Carneiro's paper on the type theory of Lean and the 2nd to last question of the FAQ.

For the second question, does:

#print axioms <name>

give you what you want? There's also a #where command in mathlib which will give you some more detailed environment info as well.

Karl Palmskog (Jan 12 2019 at 06:49):

hmm, assumptions seem to be different from axioms (section variables apparently don't count). But I guess print axioms can give some hint of what has been added.

Reid Barton (Jan 12 2019 at 07:23):

Section variables are added to the types of any definitions in the section which use them, and so they would be supplied where that definition is used.

Last updated: Dec 20 2023 at 11:08 UTC