Lean4
/-- Helper function for `proxy_equiv% type : expectedType` elaborators.
Elaborate `type` and get its `InductiveVal`. Uses the `expectedType`, where the
expected type should be of the form `_ ≃ type`. -/
def elabProxyEquiv (type : Term) (expectedType? : Option Expr) : TermElabM (Expr × InductiveVal) := do
let type ← Term.elabType type
if let some expectedType := expectedType? then
let equivType ← Term.elabType (← `(_ ≃ $(← Term.exprToSyntax type)))
unless ← isDefEq expectedType equivType do
throwError "Could not unify expected type{(indentExpr expectedType)}\nwith{indentExpr equivType}"
let type ← Term.tryPostponeIfHasMVars type "In proxy_equiv% elaborator"
let type ← whnf type
let .const declName _ := type.getAppFn |
throwError "{type} is not a constant or constant application"
return (type, ← getConstInfoInduct declName)
