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
103 lines
2.5 KiB
Text
103 lines
2.5 KiB
Text
import Lean.Meta
|
||
|
||
open Lean
|
||
open Lean.Meta
|
||
|
||
def print (msg : MessageData) : MetaM Unit := do
|
||
trace[Meta.debug] msg
|
||
|
||
def checkM (x : MetaM Bool) : MetaM Unit :=
|
||
unless (← x) do throwError "check failed"
|
||
|
||
def nat := mkConst `Nat
|
||
def boolE := mkConst `Bool
|
||
def succ := mkConst `Nat.succ
|
||
def zero := mkConst `Nat.zero
|
||
def add := mkConst `Nat.add
|
||
def io := mkConst `IO
|
||
def type := mkSort Level.one
|
||
def mkArrow (d b : Expr) : Expr := mkForall `_ BinderInfo.default d b
|
||
|
||
def tst1 : MetaM Unit := do
|
||
print "----- tst1 -----";
|
||
let m1 ← mkFreshExprMVar (mkArrow nat nat);
|
||
let lhs := mkApp m1 zero;
|
||
let rhs := zero;
|
||
checkM $ fullApproxDefEq $ isDefEq lhs rhs;
|
||
pure ()
|
||
|
||
set_option pp.all true
|
||
|
||
#eval tst1
|
||
|
||
set_option trace.Meta.debug true
|
||
|
||
def tst2 : MetaM Unit := do
|
||
print "----- tst2 -----";
|
||
let ps ← getParamNames `Or.casesOn; print (toString ps);
|
||
let ps ← getParamNames `Iff.rec; print (toString ps);
|
||
let ps ← getParamNames `checkM; print (toString ps);
|
||
pure ()
|
||
|
||
#eval tst2
|
||
|
||
axiom t1 : [Unit] = []
|
||
axiom t2 : 0 > 5
|
||
|
||
def tst3 : MetaM Unit := do
|
||
let env ← getEnv;
|
||
let t2 ← getConstInfo `t2;
|
||
let c ← mkNoConfusion t2.type (mkConst `t1);
|
||
print c;
|
||
check c;
|
||
let cType ← inferType c;
|
||
print cType;
|
||
let lt ← mkLt (mkNatLit 10000000) (mkNatLit 20000000000);
|
||
let ltPrf ← mkDecideProof lt;
|
||
check ltPrf;
|
||
let t ← inferType ltPrf;
|
||
print t;
|
||
pure ()
|
||
|
||
#eval tst3
|
||
|
||
inductive Vec.{u} (α : Type u) : Nat → Type u
|
||
| nil : Vec α 0
|
||
| cons {n : Nat} : α → Vec α n → Vec α (n+1)
|
||
|
||
def tst4 : MetaM Unit :=
|
||
withLocalDeclD `x nat fun x =>
|
||
withLocalDeclD `y nat fun y => do
|
||
let vType ← mkAppM `Vec #[nat, x];
|
||
withLocalDeclD `v vType fun v => do
|
||
let m ← mkFreshExprSyntheticOpaqueMVar vType;
|
||
let subgoals ← caseValues m.mvarId! x.fvarId! #[mkNatLit 2, mkNatLit 3, mkNatLit 5];
|
||
subgoals.forM fun s => do {
|
||
print (MessageData.ofGoal s.mvarId);
|
||
s.mvarId.assumption
|
||
};
|
||
let t ← instantiateMVars m;
|
||
print t;
|
||
check t;
|
||
pure ()
|
||
|
||
#eval tst4
|
||
|
||
def tst5 : MetaM Unit := do
|
||
let arrayNat ← mkAppM `Array #[nat];
|
||
withLocalDeclD `a arrayNat fun a => do
|
||
withLocalDeclD `b arrayNat fun b => do
|
||
let motiveType := _root_.mkArrow arrayNat (mkSort Level.zero);
|
||
withLocalDeclD `motive motiveType fun motive => do
|
||
let mvarType := mkApp motive a;
|
||
let mvar ← mkFreshExprSyntheticOpaqueMVar mvarType;
|
||
let subgoals ← caseArraySizes mvar.mvarId! a.fvarId! #[1, 0, 4, 5];
|
||
subgoals.forM fun s => do {
|
||
print (MessageData.ofGoal s.mvarId);
|
||
pure ()
|
||
};
|
||
pure ()
|
||
|
||
set_option trace.Meta.synthInstance false
|
||
|
||
#eval tst5
|