Lean trusted base

Stream: general

[Karl Palmskog]

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]

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]

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]

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.