Deduction rules of the type theory of Lean

Stream: general

[Mario Weitzer]

Is there a list of the exact formal deduction rules of the type theory used in Lean 3 and/or Lean 4 (i.e. in the format “a list of judgements (premises), horizontal line, judgement (conclusion)”)? I know it’s something like the calculus of constructions with universes and inductive types but what exactly? I checked all the resources and documentation I could find but there seems to be no succinct formal summary of the type theoretic foundation within any of them.

[Johan Commelin]

See #leantt

[Mario Weitzer]

Perfect, thank you very much!