File tree 1 file changed +0
-5
lines changed 1 file changed +0
-5
lines changed Original file line number Diff line number Diff line change @@ -129,16 +129,11 @@ def testMatchProof : (n : Nat) → Fin n → Unit
129
129
130
130
/--
131
131
info: testMatchProof (n : Nat) : Fin n → Unit
132
- testMatchProof._cstage1 (n : Nat) : Fin n → Unit
133
- testMatchProof._cstage2 : _obj → _obj → _obj
134
132
testMatchProof._sunfold (n : Nat) : Fin n → Unit
135
133
testMatchProof._unsafe_rec (n : Nat) : Fin n → Unit
136
134
testMatchProof.match_1.{u_1} (motive : (x : Nat) → Fin x → Sort u_1) (x✝ : Nat) (x✝¹ : Fin x✝)
137
135
(h_1 : (n : Nat) → (isLt : 0 < n) → motive n ⟨0, isLt⟩)
138
136
(h_2 : (as i : Nat) → (h : i.succ < as.succ) → motive as.succ ⟨i.succ, h⟩) : motive x✝ x✝¹
139
- testMatchProof.match_1._cstage1.{u_1} (motive : (x : Nat) → Fin x → Sort u_1) (x✝ : Nat) (x✝¹ : Fin x✝)
140
- (h_1 : (n : Nat) → (isLt : 0 < n) → motive n ⟨0, isLt⟩)
141
- (h_2 : (as i : Nat) → (h : i.succ < as.succ) → motive as.succ ⟨i.succ, h⟩) : motive x✝ x✝¹
142
137
testMatchProof.proof_1 (as i : Nat) (h : i.succ < as.succ) : i.succ ≤ as
143
138
testMatchProof.proof_2 (as i : Nat) (h : i.succ < as.succ) : i.succ ≤ as
144
139
-/
You can’t perform that action at this time.
0 commit comments