The definition of twelveA uses Expr.const ``Eq []. But Eq is universe-polymorphic. It probably should be Expr.const ``Eq [1] (because Nat : Sort 1).
However,
#eval show MetaM _ from do
ppExpr (← twelveA)
indeed does evaluate without error when using Expr.const ``Eq [].
The type gets pretty-printed differently ((n : Nat) → Eq Nat n (Nat.add n 1)) than for twelveB (∀ (n : Nat), n = Nat.add n 1). With Expr.const ``Eq [1] it gets pretty-printed in the same way.
The definition of
twelveAusesExpr.const ``Eq []. ButEqis universe-polymorphic. It probably should beExpr.const ``Eq [1](becauseNat : Sort 1).However,
indeed does evaluate without error when using
Expr.const ``Eq [].The type gets pretty-printed differently (
(n : Nat) → Eq Nat n (Nat.add n 1)) than fortwelveB(∀ (n : Nat), n = Nat.add n 1). WithExpr.const ``Eq [1]it gets pretty-printed in the same way.