Skip to content

Commit

Permalink
chore: space after ← in tactics (#8791)
Browse files Browse the repository at this point in the history
Co-authored-by: Moritz Firsching <firsching@google.com>
  • Loading branch information
mo271 and mo271 committed Dec 4, 2023
1 parent 19096ec commit 65c51ee
Show file tree
Hide file tree
Showing 11 changed files with 23 additions and 23 deletions.
2 changes: 1 addition & 1 deletion Mathlib/Lean/Meta.lean
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ def applyConst (mvar : MVarId) (c : Name) (cfg : ApplyConfig := {}) : MetaM (Lis
def existsi (mvar : MVarId) (es : List Expr) : MetaM MVarId := do
es.foldlM (λ mv e => do
let (subgoals,_) ← Elab.Term.TermElabM.run $ Elab.Tactic.run mv do
Elab.Tactic.evalTactic (←`(tactic| refine ⟨?_,?_⟩))
Elab.Tactic.evalTactic (← `(tactic| refine ⟨?_,?_⟩))
let [sg1, sg2] := subgoals | throwError "expected two subgoals"
sg1.assign e
pure sg2)
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/Lift.lean
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ def Lift.main (e t : TSyntax `term) (hUsing : Option (TSyntax `term))
(.tuple Syntax.missing <| [newVarName, newEqName].map (.one Syntax.missing)) goal)
-- if we use a new variable, then substitute it everywhere
if isNewVar then
for decl in ←getLCtx do
for decl in getLCtx do
if decl.userName != newEqName then
let declIdent := mkIdent decl.userName
-- The line below fails if $declIdent is there only once.
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Tactic/Linarith/Datatypes.lean
Original file line number Diff line number Diff line change
Expand Up @@ -318,7 +318,7 @@ open Meta
structure LinarithConfig : Type where
/-- Discharger to prove that a candidate linear combination of hypothesis is zero. -/
-- TODO There should be a def for this, rather than calling `evalTactic`?
discharger : TacticM Unit := do evalTactic (←`(tactic| ring1))
discharger : TacticM Unit := do evalTactic (← `(tactic| ring1))
-- We can't actually store a `Type` here,
-- as we want `LinarithConfig : Type` rather than ` : Type 1`,
-- so that we can define `elabLinarithConfig : Lean.Syntax → Lean.Elab.TermElabM LinarithConfig`.
Expand Down Expand Up @@ -346,7 +346,7 @@ since this is typically needed when using stronger unification.
def LinarithConfig.updateReducibility (cfg : LinarithConfig) (reduce_default : Bool) :
LinarithConfig :=
if reduce_default then
{ cfg with transparency := .default, discharger := do evalTactic (←`(tactic| ring1!)) }
{ cfg with transparency := .default, discharger := do evalTactic (← `(tactic| ring1!)) }
else cfg

/-!
Expand Down
16 changes: 8 additions & 8 deletions Mathlib/Tactic/MkIffOfInductiveProp.lean
Original file line number Diff line number Diff line change
Expand Up @@ -144,16 +144,16 @@ do let type := (← getConstInfo c).instantiateTypeLevelParams univs
let eqs ← eqs.mapM (λ⟨idx, inst⟩ => do
let ty ← idx.fvarId!.getType
let instTy ← inferType inst
let u := (←inferType ty).sortLevel!
if ←isDefEq ty instTy
let u := (← inferType ty).sortLevel!
if isDefEq ty instTy
then pure (mkApp3 (mkConst `Eq [u]) ty idx inst)
else pure (mkApp4 (mkConst `HEq [u]) ty idx instTy inst))
let (n, r) ← match bs.filterMap id, eqs with
| [], [] => do
pure (some 0, (mkConst `True))
| bs', [] => do
let t : Expr ← bs'.getLast!.fvarId!.getType
let l := (←inferType t).sortLevel!
let l := (← inferType t).sortLevel!
if l == Level.zero then do
let r ← mkExistsList (List.init bs') t
pure (none, subst r)
Expand All @@ -172,15 +172,15 @@ def splitThenConstructor (mvar : MVarId) (n : Nat) : MetaM Unit :=
match n with
| 0 => do
let (subgoals',_) ← Term.TermElabM.run $ Tactic.run mvar do
Tactic.evalTactic (←`(tactic| constructor))
Tactic.evalTactic (← `(tactic| constructor))
let [] := subgoals' | throwError "expected no subgoals"
pure ()
| n + 1 => do
let (subgoals,_) ← Term.TermElabM.run $ Tactic.run mvar do
Tactic.evalTactic (←`(tactic| refine ⟨?_,?_⟩))
Tactic.evalTactic (← `(tactic| refine ⟨?_,?_⟩))
let [sg1, sg2] := subgoals | throwError "expected two subgoals"
let (subgoals',_) ← Term.TermElabM.run $ Tactic.run sg1 do
Tactic.evalTactic (←`(tactic| constructor))
Tactic.evalTactic (← `(tactic| constructor))
let [] := subgoals' | throwError "expected no subgoals"
splitThenConstructor sg2 n

Expand Down Expand Up @@ -277,7 +277,7 @@ def toInductive (mvar : MVarId) (cs : List Name)
) mv3
pure (mv4, fvars)
mvar'.withContext do
let fvarIds := (←getLCtx).getFVarIds.toList
let fvarIds := (← getLCtx).getFVarIds.toList
let gs := fvarIds.take gs.length
let hs := (fvarIds.reverse.take n).reverse
let m := gs.map some ++ listBoolMerge bs hs
Expand Down Expand Up @@ -311,7 +311,7 @@ def mkIffOfInductivePropImpl (ind : Name) (rel : Name) (relStx : Syntax) : MetaM
let fvars' := fvars.toList
let shape_rhss ← constrs.mapM (constrToProp univs (fvars'.take params) (fvars'.drop params))
let (shape, rhss) := shape_rhss.unzip
pure (←mkForallFVars fvars (mkApp2 (mkConst `Iff) lhs (mkOrList rhss)),
pure (← mkForallFVars fvars (mkApp2 (mkConst `Iff) lhs (mkOrList rhss)),
shape)

let mvar ← mkFreshExprMVar (some thmTy)
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/Nontriviality/Core.lean
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ including `Subsingleton.le` and `eq_iff_true_of_subsingleton`.
-/
def nontrivialityByElim (α : Q(Type u)) (g : MVarId) (simpArgs : Array Syntax) : MetaM MVarId := do
let p : Q(Prop) ← g.getType
guard (←instantiateMVars (← inferType p)).isProp
guard (← instantiateMVars (← inferType p)).isProp
g.withContext do
let g₁ ← mkFreshExprMVarQ q(Subsingleton $α → $p)
let (_, g₁') ← g₁.mvarId!.intro1
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Tactic/PushNeg.lean
Original file line number Diff line number Diff line change
Expand Up @@ -77,12 +77,12 @@ def transformNegationStep (e : Expr) : SimpM (Option Simp.Step) := do
return mkSimpStep e (← mkAppM ``not_not_eq #[e])
| (``And, #[p, q]) =>
match ← getBoolOption `push_neg.use_distrib with
| false => return mkSimpStep (.forallE `_ p (mkNot q) default) (←mkAppM ``not_and_eq #[p, q])
| true => return mkSimpStep (mkOr (mkNot p) (mkNot q)) (←mkAppM ``not_and_or_eq #[p, q])
| false => return mkSimpStep (.forallE `_ p (mkNot q) default) (← mkAppM ``not_and_eq #[p, q])
| true => return mkSimpStep (mkOr (mkNot p) (mkNot q)) (← mkAppM ``not_and_or_eq #[p, q])
| (``Or, #[p, q]) =>
return mkSimpStep (mkAnd (mkNot p) (mkNot q)) (←mkAppM ``not_or_eq #[p, q])
return mkSimpStep (mkAnd (mkNot p) (mkNot q)) (← mkAppM ``not_or_eq #[p, q])
| (``Iff, #[p, q]) =>
return mkSimpStep (mkOr (mkAnd p (mkNot q)) (mkAnd (mkNot p) q)) (←mkAppM ``not_iff #[p, q])
return mkSimpStep (mkOr (mkAnd p (mkNot q)) (mkAnd (mkNot p) q)) (← mkAppM ``not_iff #[p, q])
| (``Eq, #[ty, e₁, e₂]) =>
if ty.isAppOfArity ``Set 1 then
-- test if equality is of the form `s = ∅`, and negate it to `s.Nonempty`
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/Rewrites.lean
Original file line number Diff line number Diff line change
Expand Up @@ -246,7 +246,7 @@ def rewritesCore (hyps : Array (Expr × Bool × Nat))
let some expr ← (match lem with
| .inl hyp => pure (some hyp)
| .inr lem => try? <| mkConstWithFreshMVarLevels lem) | return none
trace[Tactic.rewrites] m!"considering {if symm then "" else ""}{expr}"
trace[Tactic.rewrites] m!"considering {if symm then " " else ""}{expr}"
let some result ← try? do goal.rewrite target expr symm
| return none
if result.mvarIds.isEmpty then
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/SimpRw.lean
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,6 @@ elab s:"simp_rw " cfg:(config)? rws:rwRuleSeq g:(location)? : tactic => do
evalTactic (← match term with
| `(term| $e:term) =>
if symm then
`(tactic| simp%$e $[$cfg]? only [←$e:term] $g ?)
`(tactic| simp%$e $[$cfg]? only [← $e:term] $g ?)
else
`(tactic| simp%$e $[$cfg]? only [$e:term] $g ?))
4 changes: 2 additions & 2 deletions Mathlib/Tactic/SplitIfs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ private def splitIf1 (cond : Expr) (hName : Name) (loc : Location) : TacticM Uni
list is empty.
-/
private def getNextName (hNames: IO.Ref (List (TSyntax `Lean.binderIdent))) : MetaM Name := do
match ←hNames.get with
match hNames.get with
| [] => mkFreshUserName `h
| n::ns => do hNames.set ns
if let `(binderIdent| $x:ident) := n
Expand All @@ -104,7 +104,7 @@ private partial def splitIfsCore
(hNames : IO.Ref (List (TSyntax `Lean.binderIdent))) :
List Expr → TacticM Unit := fun done ↦ withMainContext do
let some (_,cond) ← findIfCondAt loc
| Meta.throwTacticEx `split_ifs (←getMainGoal) "no if-then-else conditions to split"
| Meta.throwTacticEx `split_ifs (← getMainGoal) "no if-then-else conditions to split"

-- If `cond` is `¬p` then use `p` instead.
let cond := if cond.isAppOf `Not then cond.getAppArgs[0]! else cond
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/Tauto.lean
Original file line number Diff line number Diff line change
Expand Up @@ -169,7 +169,7 @@ def tautoCore : TacticM Unit := do
distribNot <;>
liftMetaTactic (casesMatching casesMatcher (recursive := true) (throwOnNoMatch := false)) <;>
(do _ ← tryTactic (evalTactic (← `(tactic| contradiction)))) <;>
(do _ ← tryTactic (evalTactic (←`(tactic| refine or_iff_not_imp_left.mpr ?_)))) <;>
(do _ ← tryTactic (evalTactic (← `(tactic| refine or_iff_not_imp_left.mpr ?_)))) <;>
liftMetaTactic (fun m => do pure [(← m.intros!).2]) <;>
liftMetaTactic (constructorMatching · coreConstructorMatcher
(recursive := true) (throwOnNoMatch := false)) <;>
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/Widget/Conv.lean
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ private def solveLevel (expr : Expr) (path : List Nat) : MetaM SolveReturn := ma
-- we go through the application until we reach the end, counting how many explicit arguments
-- it has and noting whether they are explicit or implicit
while descExp.isApp do
if (←Lean.Meta.inferType descExp.appFn!).bindingInfo!.isExplicit then
if (← Lean.Meta.inferType descExp.appFn!).bindingInfo!.isExplicit then
explicitList := true::explicitList
count := count + 1
else
Expand Down

0 comments on commit 65c51ee

Please sign in to comment.