Mario Carneiro

feat: add `withIsShared` utility function

16

This adds two combinators for working directly with uniqueness: ```lean @[extern] def withSquashIsShared (a : α) (f : α → Squash Bool → β) : β def withIsShared (a :...

This makes the type a bit less error-prone, by not exposing the constructor or eliminator for the type (which is almost certainly an error given that elements of this type...

```lean example (h : P) : P ∨ Q := by apply .inl -- type mismatch -- Or.inl -- has type -- ?m.23 → ?m.23 ∨ ?m.24 : Prop --...

this works: ```lean example (h : P ∨ Q) : True := by cases h case _ hpq => trivial case _ hpr => trivial ``` but this doesn't: ```lean...

Completion for tactics

1

easy: ```lean example : 1 + 1 = 2 := by sim --^ textDocument/completion ``` harder: ```lean example : 1 + 1 = 2 := by skip --^ textDocument/completion done...

```lean example [Monad m] [LawfulMonad m] (h : a) : foo a := sorry --^ $/lean/plainTermGoal ``` ``` PANIC at Lean.MetavarContext.getDecl Lean.MetavarContext:370:17: unknown metavariable backtrace: libleanshared.so(+0x30f516c)[0x7f741be3516c] libleanshared.so(lean_panic_fn+0xc4)[0x7f741be354d4] libleanshared.so(l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitMain___at___private_Lean_Meta_PPGoal_0__Lean_Meta_ToHide_findDeps___spec__10+0x90c)[0x7f7419fa66cc] libleanshared.so(l___private_Lean_Meta_PPGoal_0__Lean_Meta_ToHide_findDeps+0x7d4)[0x7f7419faa874] libleanshared.so(l_Lean_Meta_ToHide_hasInaccessibleNameDep+0x115)[0x7f7419fadfe5]...

Lean 3: ```lean @[elab_as_eliminator] theorem eq.subst' {α} {motive : α → Prop} {a b : α} : a = b → motive a → motive b := eq.subst example {α}...

```lean macro (priority := high) "let " x:ident : tactic => `(let' $x := ?_) example : True := by let x exact Nat -- expected ':=' or '|' ```...

```lean import Lean #check elabTermEnsuringType --^ textDocument/completion ``` returns no result, even though the document symbols (ctrl-T) request does reveal `Lean.Elab.Term.elabTermEnsuringType` and `Lean.Elab.Tactic.elabTermEnsuringType`. This is a regression compared to lean...

```lean example : True := by { skip; trivial } ``` fails with a parse error unless the indentation of `trivial` is greater or equal to the column of `skip`....