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
24 lines
689 B
Text
24 lines
689 B
Text
import Lean
|
||
|
||
inductive Vec (α : Type u) : Nat → Type u
|
||
| nil : Vec α 0
|
||
| cons : α → Vec α n → Vec α (n+1)
|
||
|
||
def Vec.map (f : α → β) : Vec α n → Vec β n
|
||
| nil => nil
|
||
| cons a as => cons (f a) (map f as)
|
||
|
||
open Lean
|
||
open Lean.Meta
|
||
|
||
def tstHCongr (f : Expr) : MetaM Unit := do
|
||
let result ← mkHCongr f
|
||
check result.proof
|
||
IO.println (← ppExpr result.type)
|
||
IO.println (← ppExpr result.proof)
|
||
unless (← isDefEq result.type (← inferType result.proof)) do
|
||
throwError "invalid proof"
|
||
|
||
#eval tstHCongr (mkConst ``Vec.map [Level.zero, Level.zero])
|
||
|
||
#eval tstHCongr (mkApp2 (mkConst ``Vec.map [Level.zero, Level.zero]) (mkConst ``Nat) (mkConst ``Nat))
|