Eric Wieser

This file seems to frequently confuse `WithBot.some` and `Option.some`, and some of the lemmas are strange as a result. By teaching `cases` not to introduce `Option.some`, we no longer need...

This complains on each `x :=` ```lean import Qq open Qq Lean example : MetaM Nat := do let mut x := 1 if let ~q(Prop) := q(Type) then x...

This takes a very long time to elaborate: ```lean import Lean import Qq open Lean Qq def ohNo : MetaM Unit := do let xx ← inferTypeQ q(False) let res...

This doesn't work yet.

invalid match-expression, type of pattern variable 'match_eq✝' contains metavariables

3

The following example: ```lean import Qq open Qq Lean.Meta example (qo : Q(Option Nat)) (o : Option Nat) : MetaM Unit := do match qo with | ~q(some $qx) =>...

### Prerequisites Please put an X between the brackets as you perform the following steps: * [ ] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [ ]...

Storing pi in a long double?

5

Is there any way to get hold of a `long double` `pi` to the maximum possible precision? The following only gets one at the precision of `double`: ```python p =...