1 line
89 B
Text
1 line
89 B
Text
example : ("abc".pos ⟨1⟩ (by decide_cbv)).get (by decide_cbv) = 'b' := by decide_cbv
|
example : ("abc".pos ⟨1⟩ (by decide_cbv)).get (by decide_cbv) = 'b' := by decide_cbv
|