Lean4
/-- Return `true` if `expectedType?` is `some (Finset ?α)`, throws `throwUnsupportedSyntax` if it is
`some (Set ?α)`, and returns `false` otherwise. -/
def knownToBeFinsetNotSet (expectedType? : Option Expr) : TermElabM Bool :=
-- As we want to reason about the expected type, we would like to wait for it to be available.
-- However this means that if we fall back on `elabSetBuilder` we will have postponed.
-- This is undesirable as we want set builder notation to quickly elaborate to a `Set` when no
-- expected type is available.
-- tryPostponeIfNoneOrMVar expectedType?
match expectedType? with
| some expectedType =>
match_expr expectedType with
-- If the expected type is known to be `Finset ?α`, return `true`.
| Finset _ => pure true
| Set _ => throwUnsupportedSyntax
| _ => pure false
| none => pure false
