max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/elab/forInListSpecUnivPoly.lean.out.expected
Kyle Miller 48c7a4f7d9
feat: informative metavariable hovers, better delayed assignment pretty printing (#13446) 
This PR improves metavariable pretty printing and their hovers in the
InfoView. The hovers in the InfoView now include information about
specific metavariables — it includes information such as the kind of the
metavariable, whether it is a blocked delayed assignment and which
metavariables it is blocked on, and the differences in what variables
exist the metavariable's local context. Additionally, named
metavariables now pretty print with tombstones if they are inaccessible.
Delayed assignment pretty printing now more reliably follows chains of
assignments to find the pending metavariable.

**Example hovers**

Hovering over a natural metavariable:
> `?m.7 : Sort ?u.14`
> A metavariable representing an expression that should be solved for by
unification during the elaboration process. They are created during
elaboration as placeholders for implicit arguments and by `_`
placeholder syntax.
>
> Variables absent from this metavariable's local context: `a`, `b`, `y`

Hovering over `?baz`, a tactic goal:
> `?baz : ∀ (a : ?m.7) (a : ?m.8), True`
> A metavariable representing a tactic goal or an expression whose
elaboration is still pending. They usually act like constants until they
are completely solved for. They can be created using `?_` and `?n`
synthetic placeholder syntax.
>
> Variables absent from this metavariable's local context: `a`, `b`, `y`

Hovering over `?refine_1`, which appears under a binder:
> `?m.4 x : Nat`
> A metavariable representing a tactic goal or an expression whose
elaboration is still pending. They usually act like constants until they
are completely solved for. They can be created using `?_` and `?n`
synthetic placeholder syntax.
>
> This metavariable appears here via a *delayed assignment*.
Substitution is delayed until the metavariable's value contains no
metavariables, since all occurrences of the variables from its local
context will need to be replaced with expressions that are valid in the
current context.
>
> Additional variable in this metavariable's local context: `x`

Hovering over `?m.4`:
> `?m.4 : Nat → Nat`
> Part of the encoding of the *delayed assignment* mechanism. Represents
the metavariable `?refine_1`, which has additional local context
variables. Substitution is delayed until the metavariable's value
contains no metavariables, since all occurrences of the variables from
its local context will need to be replaced with expressions that are
valid in the current context.
>
> Additional variable in this metavariable's local context: `x`

The middle paragraph for `?refine_1` when it has been partially
assigned:
> This metavariable has been assigned, but it is a *delayed assignment*.
Substitution is delayed until the metavariable's value contains no
metavariables, since all occurrences of the variables from its local
context will need to be replaced with expressions that are valid in the
current context. Substitution is awaiting assignment of the following
metavariable: `?foo`
2026-04-23 01:43:55 +00:00

781 lines
42 KiB
Text
Raw Permalink Blame History

[Elab.Tactic.Do.spec] Candidates for do
let r ←
forIn (List.range (n✝ - 1)) a✝ fun i r => do
let r ←
forIn' (List.range (n✝ - i - 1)) r fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a)
pure PUnit.unit
pure (ForInStep.yield r)
pure r.toArray: [SpecProof.global Std.Do.Spec.bind]
[Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.bind instantiates to ⦃wp⟦?x⟧ (fun a => wp⟦?f a⟧ ?Q, Prod.snd ?Q)⦄
(?x >>= ?f) ⦃?Q⦄
[Elab.Tactic.Do.spec] Specs for do
let r ←
forIn (List.range (n✝ - 1)) a✝ fun i r => do
let r ←
forIn' (List.range (n✝ - i - 1)) r fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a)
pure PUnit.unit
pure (ForInStep.yield r)
pure r.toArray: [SpecProof.global Std.Do.Spec.bind]
[Elab.Tactic.Do.spec] dischargeMGoal: wp⟦forIn (List.range (n✝ - 1)) a✝ fun i r => do
let r ←
forIn' (List.range (n✝ - i - 1)) r fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a)
pure PUnit.unit
pure (ForInStep.yield r)⟧
(fun a => wp⟦pure a.toArray⟧ (PostCond.noThrow fun a => { down := A.toList.Perm a.toList }),
(PostCond.noThrow fun a => { down := A.toList.Perm a.toList }).snd)
[Elab.Tactic.Do.spec] pureRflAndAndIntro: wp⟦forIn (List.range (n✝ - 1)) a✝ fun i r => do
let r ←
forIn' (List.range (n✝ - i - 1)) r fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a)
pure PUnit.unit
pure (ForInStep.yield r)⟧
(fun a => wp⟦pure a.toArray⟧ (PostCond.noThrow fun a => { down := A.toList.Perm a.toList }),
(PostCond.noThrow fun a => { down := A.toList.Perm a.toList }).snd)
[Elab.Tactic.Do.spec] discharge? (wp⟦forIn (List.range (n✝ - 1)) a✝ fun i r => do
let r ←
forIn' (List.range (n✝ - i - 1)) r fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a)
pure PUnit.unit
pure (ForInStep.yield r)⟧
(fun a => wp⟦pure a.toArray⟧ (PostCond.noThrow fun a => { down := A.toList.Perm a.toList }),
(PostCond.noThrow fun a => { down := A.toList.Perm a.toList }).snd)).down
[Elab.Tactic.Do.spec] pure Prop: (wp⟦forIn (List.range (n✝ - 1)) a✝ fun i r => do
let r ←
forIn' (List.range (n✝ - i - 1)) r fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a)
pure PUnit.unit
pure (ForInStep.yield r)⟧
(fun a => wp⟦pure a.toArray⟧ (PostCond.noThrow fun a => { down := A.toList.Perm a.toList }),
(PostCond.noThrow fun a => { down := A.toList.Perm a.toList }).snd)).down
[Elab.Tactic.Do.spec] Candidates for forIn (List.range (n✝ - 1)) a✝ fun i r => do
let r ←
forIn' (List.range (n✝ - i - 1)) r fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a)
pure PUnit.unit
pure (ForInStep.yield r): [SpecProof.global Std.Do.Spec.forIn_list]
[Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.forIn_list instantiates to ⦃Prod.fst ?inv
({ «prefix» := [], suffix := ?xs, property := ⋯ }, ?init)⦄
forIn ?xs ?init ?f ⦃(fun b => Prod.fst ?inv ({ «prefix» := ?xs, suffix := [], property := ⋯ }, b), Prod.snd ?inv)⦄
[Elab.Tactic.Do.spec] Specs for forIn (List.range (n✝ - 1)) a✝ fun i r => do
let r ←
forIn' (List.range (n✝ - i - 1)) r fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a)
pure PUnit.unit
pure (ForInStep.yield r): [SpecProof.global Std.Do.Spec.forIn_list]
[Elab.Tactic.Do.spec] dischargeMGoal: Prod.fst ?inv
({ «prefix» := [], suffix := List.range (n✝ - 1), property := ⋯ }, a✝)
[Elab.Tactic.Do.spec] pureRflAndAndIntro: Prod.fst ?inv
({ «prefix» := [], suffix := List.range (n✝ - 1), property := ⋯ }, a✝)
[Elab.Tactic.Do.spec] discharge? (Prod.fst ?inv
({ «prefix» := [], suffix := List.range (n✝ - 1), property := ⋯ }, a✝)).down
[Elab.Tactic.Do.spec] pure Prop: (Prod.fst ?inv
({ «prefix» := [], suffix := List.range (n✝ - 1), property := ⋯ }, a✝)).down
[Elab.Tactic.Do.spec] Candidates for do
let r ←
forIn' (List.range (n✝ - cur - 1)) b fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a)
pure PUnit.unit
pure (ForInStep.yield r): [SpecProof.global Std.Do.Spec.bind]
[Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.bind instantiates to ⦃wp⟦?x⟧ (fun a => wp⟦?f a⟧ ?Q, Prod.snd ?Q)⦄
(?x >>= ?f) ⦃?Q⦄
[Elab.Tactic.Do.spec] Specs for do
let r ←
forIn' (List.range (n✝ - cur - 1)) b fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a)
pure PUnit.unit
pure (ForInStep.yield r): [SpecProof.global Std.Do.Spec.bind]
[Elab.Tactic.Do.spec] dischargeMGoal: wp⟦forIn' (List.range (n✝ - cur - 1)) b fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a)⟧
(fun a =>
wp⟦do
pure PUnit.unit
pure (ForInStep.yield a)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd)
[Elab.Tactic.Do.spec] pureRflAndAndIntro: wp⟦forIn' (List.range (n✝ - cur - 1)) b fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a)⟧
(fun a =>
wp⟦do
pure PUnit.unit
pure (ForInStep.yield a)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd)
[Elab.Tactic.Do.spec] discharge? (wp⟦forIn' (List.range (n✝ - cur - 1)) b fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a)⟧
(fun a =>
wp⟦do
pure PUnit.unit
pure (ForInStep.yield a)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd)).down
[Elab.Tactic.Do.spec] pure Prop: (wp⟦forIn' (List.range (n✝ - cur - 1)) b fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a)⟧
(fun a =>
wp⟦do
pure PUnit.unit
pure (ForInStep.yield a)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd)).down
[Elab.Tactic.Do.spec] Candidates for forIn' (List.range (n✝ - cur - 1)) b fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a): [SpecProof.global Std.Do.Spec.forIn'_list]
[Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.forIn'_list instantiates to ⦃Prod.fst ?inv
({ «prefix» := [], suffix := ?xs, property := ⋯ }, ?init)⦄
forIn' ?xs ?init
?f ⦃(fun b => Prod.fst ?inv ({ «prefix» := ?xs, suffix := [], property := ⋯ }, b), Prod.snd ?inv)⦄
[Elab.Tactic.Do.spec] Specs for forIn' (List.range (n✝ - cur - 1)) b fun j hj r =>
have a := r;
have this := ⋯;
if a[j] > a[j + 1] then do
pure PUnit.unit
pure (ForInStep.yield (a.swap j (j + 1) ⋯ ⋯))
else do
pure PUnit.unit
pure (ForInStep.yield a): [SpecProof.global Std.Do.Spec.forIn'_list]
[Elab.Tactic.Do.spec] dischargeMGoal: Prod.fst ?inv
({ «prefix» := [], suffix := List.range (n✝ - cur - 1), property := ⋯ }, b)
[Elab.Tactic.Do.spec] pureRflAndAndIntro: Prod.fst ?inv
({ «prefix» := [], suffix := List.range (n✝ - cur - 1), property := ⋯ }, b)
[Elab.Tactic.Do.spec] discharge? (Prod.fst ?inv
({ «prefix» := [], suffix := List.range (n✝ - cur - 1), property := ⋯ }, b)).down
[Elab.Tactic.Do.spec] pure Prop: (Prod.fst ?inv
({ «prefix» := [], suffix := List.range (n✝ - cur - 1), property := ⋯ }, b)).down
[Elab.Tactic.Do.spec] Candidates for do
pure PUnit.unit
pure (ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯)): [SpecProof.global Std.Do.Spec.bind]
[Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.bind instantiates to ⦃wp⟦?x⟧ (fun a => wp⟦?f a⟧ ?Q, Prod.snd ?Q)⦄
(?x >>= ?f) ⦃?Q⦄
[Elab.Tactic.Do.spec] Specs for do
pure PUnit.unit
pure (ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯)): [SpecProof.global Std.Do.Spec.bind]
[Elab.Tactic.Do.spec] dischargeMGoal: wp⟦pure PUnit.unit⟧
(fun a =>
wp⟦pure (ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯))⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd)
[Elab.Tactic.Do.spec] pureRflAndAndIntro: wp⟦pure PUnit.unit⟧
(fun a =>
wp⟦pure (ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯))⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd)
[Elab.Tactic.Do.spec] discharge? (wp⟦pure PUnit.unit⟧
(fun a =>
wp⟦pure (ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯))⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd)).down
[Elab.Tactic.Do.spec] pure Prop: (wp⟦pure PUnit.unit⟧
(fun a =>
wp⟦pure (ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯))⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd)).down
[Elab.Tactic.Do.spec] Candidates for pure PUnit.unit: [SpecProof.global Std.Do.Spec.pure]
[Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.pure instantiates to ⦃Prod.fst ?Q ?a⦄ pure ?a ⦃?Q⦄
[Elab.Tactic.Do.spec] Specs for pure PUnit.unit: [SpecProof.global Std.Do.Spec.pure]
[Elab.Tactic.Do.spec] dischargeMGoal: (fun a =>
wp⟦pure (ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯))⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd).fst
PUnit.unit
[Elab.Tactic.Do.spec] pureRflAndAndIntro: (fun a =>
wp⟦pure (ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯))⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd).fst
PUnit.unit
[Elab.Tactic.Do.spec] discharge? ((fun a =>
wp⟦pure (ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯))⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd).fst
PUnit.unit).down
[Elab.Tactic.Do.spec] pure Prop: ((fun a =>
wp⟦pure (ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯))⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd).fst
PUnit.unit).down
[Elab.Tactic.Do.spec] Candidates for pure
(ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯)): [SpecProof.global Std.Do.Spec.pure]
[Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.pure instantiates to ⦃Prod.fst ?Q ?a⦄ pure ?a ⦃?Q⦄
[Elab.Tactic.Do.spec] Specs for pure (ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯)): [SpecProof.global Std.Do.Spec.pure]
[Elab.Tactic.Do.spec] dischargeMGoal: (fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).fst
(ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯))
[Elab.Tactic.Do.spec] pureRflAndAndIntro: (fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).fst
(ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯))
[Elab.Tactic.Do.spec] discharge? ((fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).fst
(ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯))).down
[Elab.Tactic.Do.spec] pure Prop: ((fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).fst
(ForInStep.yield (b.swap cur (cur + 1) ⋯ ⋯))).down
[Elab.Tactic.Do.spec] Candidates for do
pure PUnit.unit
pure (ForInStep.yield b): [SpecProof.global Std.Do.Spec.bind]
[Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.bind instantiates to ⦃wp⟦?x⟧ (fun a => wp⟦?f a⟧ ?Q, Prod.snd ?Q)⦄
(?x >>= ?f) ⦃?Q⦄
[Elab.Tactic.Do.spec] Specs for do
pure PUnit.unit
pure (ForInStep.yield b): [SpecProof.global Std.Do.Spec.bind]
[Elab.Tactic.Do.spec] dischargeMGoal: wp⟦pure PUnit.unit⟧
(fun a =>
wp⟦pure (ForInStep.yield b)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd)
[Elab.Tactic.Do.spec] pureRflAndAndIntro: wp⟦pure PUnit.unit⟧
(fun a =>
wp⟦pure (ForInStep.yield b)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd)
[Elab.Tactic.Do.spec] discharge? (wp⟦pure PUnit.unit⟧
(fun a =>
wp⟦pure (ForInStep.yield b)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd)).down
[Elab.Tactic.Do.spec] pure Prop: (wp⟦pure PUnit.unit⟧
(fun a =>
wp⟦pure (ForInStep.yield b)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd)).down
[Elab.Tactic.Do.spec] Candidates for pure PUnit.unit: [SpecProof.global Std.Do.Spec.pure]
[Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.pure instantiates to ⦃Prod.fst ?Q ?a⦄ pure ?a ⦃?Q⦄
[Elab.Tactic.Do.spec] Specs for pure PUnit.unit: [SpecProof.global Std.Do.Spec.pure]
[Elab.Tactic.Do.spec] dischargeMGoal: (fun a =>
wp⟦pure (ForInStep.yield b)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd).fst
PUnit.unit
[Elab.Tactic.Do.spec] pureRflAndAndIntro: (fun a =>
wp⟦pure (ForInStep.yield b)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd).fst
PUnit.unit
[Elab.Tactic.Do.spec] discharge? ((fun a =>
wp⟦pure (ForInStep.yield b)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd).fst
PUnit.unit).down
[Elab.Tactic.Do.spec] pure Prop: ((fun a =>
wp⟦pure (ForInStep.yield b)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).snd).fst
PUnit.unit).down
[Elab.Tactic.Do.spec] Candidates for pure (ForInStep.yield b): [SpecProof.global Std.Do.Spec.pure]
[Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.pure instantiates to ⦃Prod.fst ?Q ?a⦄ pure ?a ⦃?Q⦄
[Elab.Tactic.Do.spec] Specs for pure (ForInStep.yield b): [SpecProof.global Std.Do.Spec.pure]
[Elab.Tactic.Do.spec] dischargeMGoal: (fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).fst
(ForInStep.yield b)
[Elab.Tactic.Do.spec] pureRflAndAndIntro: (fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).fst
(ForInStep.yield b)
[Elab.Tactic.Do.spec] discharge? ((fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).fst
(ForInStep.yield b)).down
[Elab.Tactic.Do.spec] pure Prop: ((fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv ({ «prefix» := List.range (n✝ - cur✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv).fst
(ForInStep.yield b)).down
[Elab.Tactic.Do.spec] Candidates for do
pure PUnit.unit
pure (ForInStep.yield r✝): [SpecProof.global Std.Do.Spec.bind]
[Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.bind instantiates to ⦃wp⟦?x⟧ (fun a => wp⟦?f a⟧ ?Q, Prod.snd ?Q)⦄
(?x >>= ?f) ⦃?Q⦄
[Elab.Tactic.Do.spec] Specs for do
pure PUnit.unit
pure (ForInStep.yield r✝): [SpecProof.global Std.Do.Spec.bind]
[Elab.Tactic.Do.spec] dischargeMGoal: wp⟦pure PUnit.unit⟧
(fun a =>
wp⟦pure (ForInStep.yield r✝)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝).snd)
[Elab.Tactic.Do.spec] pureRflAndAndIntro: wp⟦pure PUnit.unit⟧
(fun a =>
wp⟦pure (ForInStep.yield r✝)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝).snd)
[Elab.Tactic.Do.spec] discharge? (wp⟦pure PUnit.unit⟧
(fun a =>
wp⟦pure (ForInStep.yield r✝)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝).snd)).down
[Elab.Tactic.Do.spec] pure Prop: (wp⟦pure PUnit.unit⟧
(fun a =>
wp⟦pure (ForInStep.yield r✝)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝).snd)).down
[Elab.Tactic.Do.spec] Candidates for pure PUnit.unit: [SpecProof.global Std.Do.Spec.pure]
[Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.pure instantiates to ⦃Prod.fst ?Q ?a⦄ pure ?a ⦃?Q⦄
[Elab.Tactic.Do.spec] Specs for pure PUnit.unit: [SpecProof.global Std.Do.Spec.pure]
[Elab.Tactic.Do.spec] dischargeMGoal: (fun a =>
wp⟦pure (ForInStep.yield r✝)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝).snd).fst
PUnit.unit
[Elab.Tactic.Do.spec] pureRflAndAndIntro: (fun a =>
wp⟦pure (ForInStep.yield r✝)⟧
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝),
(fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝).snd).fst
PUnit.unit
[Elab.Tactic.Do.spec] discharge? ((fun a =>
wp⟦pure (ForInStep.yield r✝)⟧
(fun r =>
match r with
| ForInStep.yield b' =>
Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝),
(fun r =>
match r with
| ForInStep.yield b' =>
Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝).snd).fst
PUnit.unit).down
[Elab.Tactic.Do.spec] pure Prop: ((fun a =>
wp⟦pure (ForInStep.yield r✝)⟧
(fun r =>
match r with
| ForInStep.yield b' =>
Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝),
(fun r =>
match r with
| ForInStep.yield b' =>
Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝).snd).fst
PUnit.unit).down
[Elab.Tactic.Do.spec] Candidates for pure (ForInStep.yield r✝): [SpecProof.global Std.Do.Spec.pure]
[Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.pure instantiates to ⦃Prod.fst ?Q ?a⦄ pure ?a ⦃?Q⦄
[Elab.Tactic.Do.spec] Specs for pure (ForInStep.yield r✝): [SpecProof.global Std.Do.Spec.pure]
[Elab.Tactic.Do.spec] dischargeMGoal: (fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝).fst
(ForInStep.yield r✝)
[Elab.Tactic.Do.spec] pureRflAndAndIntro: (fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝).fst
(ForInStep.yield r✝)
[Elab.Tactic.Do.spec] discharge? ((fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝).fst
(ForInStep.yield r✝)).down
[Elab.Tactic.Do.spec] pure Prop: ((fun r =>
match r with
| ForInStep.yield b' => Prod.fst ?inv✝ ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' =>
Prod.fst ?inv✝ ({ «prefix» := List.range (n✝ - 1), suffix := [], property := ⋯ }, b'),
Prod.snd ?inv✝).fst
(ForInStep.yield r✝)).down
[Elab.Tactic.Do.spec] Candidates for pure r✝.toArray: [SpecProof.global Std.Do.Spec.pure]
[Elab.Tactic.Do.spec] SpecProof.global Std.Do.Spec.pure instantiates to ⦃Prod.fst ?Q ?a⦄ pure ?a ⦃?Q⦄
[Elab.Tactic.Do.spec] Specs for pure r✝.toArray: [SpecProof.global Std.Do.Spec.pure]
[Elab.Tactic.Do.spec] dischargeMGoal: (PostCond.noThrow fun a => { down := A.toList.Perm a.toList }).fst r✝.toArray
[Elab.Tactic.Do.spec] pureRflAndAndIntro: (PostCond.noThrow fun a => { down := A.toList.Perm a.toList }).fst r✝.toArray
[Elab.Tactic.Do.spec] discharge? ((PostCond.noThrow fun a => { down := A.toList.Perm a.toList }).fst r✝.toArray).down
[Elab.Tactic.Do.spec] pure Prop: ((PostCond.noThrow fun a => { down := A.toList.Perm a.toList }).fst r✝.toArray).down
Reference in a new issue View git blame Copy permalink