Hole commands MVP

Stream: mathlib4

[Mario Carneiro]

std4#131 implements a framework for doing hole commands similar to mathlib3, except that it doesn't have the {! !} variant, it just uses plain holes. In particular, it implements autocompletion for { a := _, b := _ } and fun | .a => _ | .b => _.

For example:

instance : Monad Id := {
  map := _
  mapConst := _
  pure := _
  seq := _
  seqLeft := _
  seqRight := _
  bind := _
}

def foo : Expr → Unit := fun
  | .bvar deBruijnIndex => _
  | .fvar fvarId => _
  | .mvar mvarId => _
  | .sort u => _
  | .const declName us => _
  | .app fn arg => _
  | .lam binderName binderType body binderInfo => _
  | .forallE binderName binderType body binderInfo => _
  | .letE declName type value body nonDep => _
  | .lit _ => _
  | .mdata data expr => _
  | .proj typeName idx struct => _