Type theory without non-trivial reflexivity proofs?

Stream: new members

[Chris M]

In the Lean tutorial it says that nontrivial identities can be proved by reflexivity. An example is :

example : 2+3=5 := eq.refl _

My understanding of how the Lean type checker does this is that it kind of "computes 2 + 5 at compile time, and if it indeed computes to 5, accepts the proof".

So in a sense, we ca think of an equality proof as a kind of "compile-time computation" that gives you a token that allows you to "skip the computation at runtime" and just grab the precomputed result.

Are there type systems (other than Lean's) where this is explicit? I.e. where you have to actually do the "compile time computation" yourself, and can only use equational reflexivity for the trivial case?

[Mario Carneiro]

Yes, metamath computations work like this, HOL too

[Mario Carneiro]

In fact I think it is a feature unique to DTT

[Mario Carneiro]

See for example http://us.metamath.org/mpeuni/2p2e4.html and note that the proof is not "by refl" but rather by a couple of applications of associativity