fix

leanprover · Dec 15, 2024 · 0c010eb · 0c010eb
1 parent 8af9462
commit 0c010eb
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 8 deletions.
diff --git a/src/Init/Data/Range.lean b/src/Init/Data/Range.lean
@@ -13,7 +13,7 @@ structure Range where
   start : Nat := 0
   stop  : Nat
   step  : Nat := 1
-  step_pos : 0 < step := by decide
+  step_pos : 0 < step
 
 instance : Membership Nat Range where
   mem r i := r.start ≤ i ∧ i < r.stop
@@ -56,10 +56,10 @@ syntax:max "[" withoutPosition(":" term ":" term) "]" : term
 syntax:max "[" withoutPosition(term ":" term ":" term) "]" : term
 
 macro_rules
-  | `([ : $stop]) => `({ stop := $stop : Range })
-  | `([ $start : $stop ]) => `({ start := $start, stop := $stop : Range })
-  | `([ $start : $stop : $step ]) => `({ start := $start, stop := $stop, step := $step : Range })
-  | `([ : $stop : $step ]) => `({ stop := $stop, step := $step : Range })
+  | `([ : $stop]) => `({ stop := $stop, step_pos := Nat.zero_lt_one : Range })
+  | `([ $start : $stop ]) => `({ start := $start, stop := $stop, step_pos := Nat.zero_lt_one : Range })
+  | `([ $start : $stop : $step ]) => `({ start := $start, stop := $stop, step := $step, step_pos := by decide : Range })
+  | `([ : $stop : $step ]) => `({ stop := $stop, step := $step, step_pos := by decide : Range })
 
 end Range
 end Std

diff --git a/src/Lean/Compiler/LCNF/Util.lean b/src/Lean/Compiler/LCNF/Util.lean
@@ -56,7 +56,7 @@ def getCasesInfo? (declName : Name) : CoreM (Option CasesInfo) := do
   let arity        := numParams + 1 /- motive -/ + val.numIndices + 1 /- major -/ + val.numCtors
   let discrPos     := numParams + 1 /- motive -/ + val.numIndices
   -- We view indices as discriminants
-  let altsRange    := { start := discrPos + 1,  stop := arity }
+  let altsRange    := [discrPos + 1:arity]
   let altNumParams ← val.ctors.toArray.mapM fun ctor => do
     let .ctorInfo ctorVal ← getConstInfo ctor | unreachable!
     return ctorVal.numFields

diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean
@@ -43,13 +43,13 @@ def MatcherInfo.getFirstDiscrPos (info : MatcherInfo) : Nat :=
   info.numParams + 1
 
 def MatcherInfo.getDiscrRange (info : MatcherInfo) : Std.Range :=
-  { start := info.getFirstDiscrPos, stop := info.getFirstDiscrPos + info.numDiscrs }
+  [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs]
 
 def MatcherInfo.getFirstAltPos (info : MatcherInfo) : Nat :=
   info.numParams + 1 + info.numDiscrs
 
 def MatcherInfo.getAltRange (info : MatcherInfo) : Std.Range :=
-  { start := info.getFirstAltPos, stop := info.getFirstAltPos + info.numAlts }
+  [info.getFirstAltPos : info.getFirstAltPos + info.numAlts]
 
 def MatcherInfo.getMotivePos (info : MatcherInfo) : Nat :=
   info.numParams