Sebastian Ullrich
Sebastian Ullrich
``` #check id -- completes here #check !id -- doesn't ``` 4.9.0, commit b0c1112471a3f38859d9738184d21132b7d9cd0c
This implements a much smaller version of #4610: we make sure that any *tactic* `have ... by` does not allow postponing mvars in the type, but do not change any...
Resolves #2452. For *theorems*, section variables are now conditionally included when elaborating the theorem body and sending the result to the kernel based on their use in the header; elaboration...
Initial options are now re-parsed and validated after importing. Cmdline option assignments prefixed with `weak.` are silently discarded if the option name without the prefix does not exist. Fixes #3403
``` import Lean example (range : String.Range) : String.Pos := ⟨range.stop.b⟩ example (p : String.Pos) : String.Pos := ⟨p.b⟩ ``` Both `b`s complete to very different lists, but neither contains...