66bc9ae177
This PR deprecates `levelZero` in favor of `Level.zero` and `levelOne`
in favor of the new `Level.one`, and updates all usages throughout the
codebase. The `levelZero` alias was previously required for computed
field `data` to work, but this is no longer needed.
🤖 Prepared with Claude Code
26 lines
642 B
Text
26 lines
642 B
Text
import Lean
|
|
|
|
|
|
/-! Pretty printing tests for `Expr`s that cannot be generated by parsing+elaborating. -/
|
|
|
|
open Lean
|
|
|
|
def test (e : Expr) : MetaM Unit := do
|
|
IO.println (← PrettyPrinter.ppExpr e)
|
|
|
|
-- loose bound variable
|
|
#eval test (mkBVar 0)
|
|
|
|
-- anonymous binder
|
|
#eval test (mkLambda Name.anonymous BinderInfo.default (mkSort Level.zero) (mkBVar 0))
|
|
|
|
-- pp annotations
|
|
#eval test $
|
|
mkAppN (mkConst `id [Level.one]) #[
|
|
mkConst `Nat,
|
|
mkMData (KVMap.empty.set `pp.explicit true) $ mkAppN (mkConst `id [Level.one]) #[
|
|
mkConst `Nat,
|
|
mkAppN (mkConst `id [Level.one]) #[
|
|
mkConst `Nat,
|
|
mkConst `Nat.zero
|
|
]]]
|