Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 0fc2480

Browse files
committedMar 21, 2025·
product type
1 parent 4cd0dfa commit 0fc2480

File tree

1 file changed

+27
-0
lines changed

1 file changed

+27
-0
lines changed
 

‎PfsProgs25/Unit13/MetaSolve.lean

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -143,3 +143,30 @@ elab "list_eg" : term => do
143143
#eval list_eg
144144

145145
#check mkSort
146+
147+
#check Prod
148+
149+
def prodExpr? (e: Expr) :
150+
MetaM <|Option (Expr × Expr) := do
151+
let u ← mkFreshLevelMVar
152+
let v ← mkFreshLevelMVar
153+
let α ← mkFreshExprMVar (mkSort <| Level.succ u)
154+
let β ← mkFreshExprMVar (mkSort <| Level.succ v)
155+
let prod ← mkAppM ``Prod #[α, β]
156+
if ← isDefEq e prod then
157+
return some (α, β)
158+
else
159+
return none
160+
161+
162+
elab "#prodExpr" "[" e:term "]" : command =>
163+
Command.liftTermElabM do
164+
let e ← elabTerm e none
165+
match ← prodExpr? e with
166+
| some (α, β) =>
167+
logInfo m!"{α} × {β}"
168+
logInfo m!"{α} has type: {← inferType α}"
169+
logInfo m!"{β} has type: {← inferType β}"
170+
| none => logInfo "Not a PProd expression"
171+
172+
#prodExpr [Nat × (Nat → Type)]

0 commit comments

Comments
 (0)
Please sign in to comment.