Main> :r
1/1: Building src.Main (src/Main.idr)
Loaded file src/Main.idr
Main> :ti todo
input : List Nat
x : ErasedThing (Equal {a = Nat} {b = Nat} (.fst {type = Nat} {pred = \returnValue : Nat =>
Equal {a = Nat} {b = Nat} returnValue (foldr {acc = Nat} {elem = Nat} maximum 0 (reverseOnto {a = Nat} ([] {a = Nat}) input))} (let Element {type = returnOut} {pred = \returnValue : returnOut =>
ComposedReturnProof {returnOut} {streamOut = Void} {streamIn = Void} {streamMid = streamIn} {returnMid = ()} (fromListReturnInvariant {streamOut = streamIn} list) (ExhaustsInputAnd {returnOut} {streamOut = Void} {streamIn} returnInvariant) (Yes () ()) ([] {a = Void}) ([] {a = Void}) returnValue} returnValue proofs =
.runIdentity {a = Subset Nat (\returnValue : Nat =>
ComposedReturnProof {returnOut = Nat} {streamOut = Void} {streamIn = Void} {streamMid = Nat} {returnMid = ()} (fromListReturnInvariant {streamOut = Nat} input) (ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} maxReturnInvariant) (Yes () ()) ([] {a = Void}) ([] {a = Void}) returnValue)} (runPipeWithInvariant {return = Nat} {returnInvariant = ComposedReturnProof {returnOut = Nat} {streamOut = Void} {streamIn = Void} {streamMid = Nat} {returnMid = ()} (fromListReturnInvariant {streamOut = Nat} input) (ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} maxReturnInvariant)} {effects = Identity} {{conArg:4374} = MkMonad {m = Identity} {{conArg:9608} = MkApplicative {f = Identity} {{conArg:9127} = MkFunctor {f = Identity} (\0 b : Type,
0 a : Type,
func : a -> b,
{arg:8429} : Identity a =>
map {b} {a} func arg)} (\0 a : Type,
{arg:9131} : a =>
Id {a} arg) (\0 b : Type,
0 a : Type,
{arg:9137} : Identity (a -> b),
{arg:9144} : Identity a =>
<*> {b} {a} arg arg)} (\0 b : Type,
0 a : Type,
{arg:9612} : Identity a,
{arg:9615} : a -> Identity b =>
>>= {b} {a} arg arg) (\0 a : Type,
{arg:9626} : Identity (Identity a) =>
>>= {b = a} {a = Identity a} arg (id {a = Identity a}))} (push Nat Void Nat (ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} maxReturnInvariant) (NoStreamInvariant {streamOut = Void} {streamIn = Nat}) ([] {a = Void}) () Void (fromListReturnInvariant {streamOut = Nat} input) (\currentHistoryIn : List Void,
currentHistoryOut : List Nat =>
DPair (List Nat) (\suffix : List Nat =>
Equal {a = List Nat} {b = List Nat} (++ {a = Nat} (reverseOnto {a = Nat} ([] {a = Nat}) currentHistoryOut) suffix) input)) ([] {a = Nat}) ([] {a = Void}) (Yes () ()) Void Identity (MkMonad {m = Identity} {{conArg:9608} = MkApplicative {f = Identity} {{conArg:9127} = MkFunctor {f = Identity} (\0 b : Type,
0 a : Type,
func : a -> b,
{arg:8429} : Identity a =>
map {b} {a} func arg)} (\0 a : Type,
{arg:9131} : a =>
Id {a} arg) (\0 b : Type,
0 a : Type,
{arg:9137} : Identity (a -> b),
{arg:9144} : Identity a =>
<*> {b} {a} arg arg)} (\0 b : Type,
0 a : Type,
{arg:9612} : Identity a,
{arg:9615} : a -> Identity b =>
>>= {b} {a} arg arg) (\0 a : Type,
{arg:9626} : Identity (Identity a) =>
>>= {b = a} {a = Identity a} arg (id {a = Identity a}))) {pushHistoryOut = [] {a = Void}} {effects' = Identity} {{conArg:3726} = MkMonad {m = Identity} {{conArg:9608} = MkApplicative {f = Identity} {{conArg:9127} = MkFunctor {f = Identity} (\0 b : Type,
0 a : Type,
func : a -> b,
{arg:8429} : Identity a =>
map {b} {a} func arg)} (\0 a : Type,
{arg:9131} : a =>
Id {a} arg) (\0 b : Type,
0 a : Type,
{arg:9137} : Identity (a -> b),
{arg:9144} : Identity a =>
<*> {b} {a} arg arg)} (\0 b : Type,
0 a : Type,
{arg:9612} : Identity a,
{arg:9615} : a -> Identity b =>
>>= {b} {a} arg arg) (\0 a : Type,
{arg:9626} : Identity (Identity a) =>
>>= {b = a} {a = Identity a} arg (id {a = Identity a}))} {pushIsInputExhaustedIn = Yes () ()} {pushHistoryIn = [] {a = Void}} {pushHistoryMid = [] {a = Nat}} (recurse Nat Identity (MkMonad {m = Identity} {{conArg:9608} = MkApplicative {f = Identity} {{conArg:9127} = MkFunctor {f = Identity} (\0 b : Type,
0 a : Type,
func : a -> b,
{arg:8429} : Identity a =>
map {b} {a} func arg)} (\0 a : Type,
{arg:9131} : a =>
Id {a} arg) (\0 b : Type,
0 a : Type,
{arg:9137} : Identity (a -> b),
{arg:9144} : Identity a =>
<*> {b} {a} arg arg)} (\0 b : Type,
0 a : Type,
{arg:9612} : Identity a,
{arg:9615} : a -> Identity b =>
>>= {b} {a} arg arg) (\0 a : Type,
{arg:9626} : Identity (Identity a) =>
>>= {b = a} {a = Identity a} arg (id {a = Identity a}))) input {{isInputExhausted:4695} = Yes () ()} {{historyIn:4694} = [] {a = Void}} {historyOut = [] {a = Nat}} input (Refl {a = List Nat} {x = input})) (\value : (),
0 {upstreamReturnProperty:1820} : Type,
0 upstreamReturnProof : upstreamReturnProperty =>
Delay (recurse Nat Void Nat (ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
Equal {a = Nat} {b = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} maximum 0 finalHistoryIn))) ([] {a = Void}) ([] {a = Nat}) No () Identity (MkMonad {m = Identity} {{conArg:9608} = MkApplicative {f = Identity} {{conArg:9127} = MkFunctor {f = Identity} (\0 b : Type,
0 a : Type,
func : a -> b,
{arg:8429} : Identity a =>
map {b} {a} func arg)} (\0 a : Type,
{arg:9131} : a =>
Id {a} arg) (\0 b : Type,
0 a : Type,
{arg:9137} : Identity (a -> b),
{arg:9144} : Identity a =>
<*> {b} {a} arg arg)} (\0 b : Type,
0 a : Type,
{arg:9612} : Identity a,
{arg:9615} : a -> Identity b =>
>>= {b} {a} arg arg) (\0 a : Type,
{arg:9626} : Identity (Identity a) =>
>>= {b = a} {a = Identity a} arg (id {a = Identity a}))) (Await {returnOut = Nat} {streamOut = Void} {streamIn = Nat} {returnInvariant = ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
Equal {a = Nat} {b = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} maximum 0 finalHistoryIn))} {streamInvariant = NoStreamInvariant {streamOut = Void} {streamIn = Nat}} {effects = Identity} {historyOut = [] {a = Void}} {historyIn = [] {a = Nat}} {returnIn = ()} (\returnValue : (),
0 {upstreamReturnProperty:5799} : Type,
0 returnProof : upstreamReturnProperty =>
Delay (Return {streamOut = Void} {streamIn = Nat} {streamInvariant = NoStreamInvariant {streamOut = Void} {streamIn = Nat}} {effects = Identity} {returnIn = ()} {historyOut = [] {a = Void}} {historyIn = [] {a = Nat}} {isInputExhausted = Yes upstreamReturnProperty returnProof} {returnOut = Nat} {returnInvariant = ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
=== {a = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} {t = List} {__con = Foldable implementation at Prelude.Types:428:1--441:59} maximum 0 finalHistoryIn))} 0 (Refl {a = Nat} {x = 0}))) (onStream Nat Nat 0 maximum 0 ([] {a = Nat}) (Refl {a = Nat} {x = 0}))) {innerReturnInvariant = ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
Equal {a = Nat} {b = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} maximum 0 finalHistoryIn))} {innerHistoryOut = [] {a = Void}} {innerHistoryIn = [] {a = Nat}} {innerIsInputExhausted = Yes upstreamReturnProperty upstreamReturnProof} (Delay (Return {streamOut = Void} {streamIn = Nat} {streamInvariant = NoStreamInvariant {streamOut = Void} {streamIn = Nat}} {effects = Identity} {returnIn = ()} {historyOut = [] {a = Void}} {historyIn = [] {a = Nat}} {isInputExhausted = Yes upstreamReturnProperty upstreamReturnProof} {returnOut = Nat} {returnInvariant = ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
=== {a = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} {t = List} {__con = Foldable implementation at Prelude.Types:428:1--441:59} maximum 0 finalHistoryIn))} 0 (Refl {a = Nat} {x = 0}))))) (\value : Nat =>
Delay (recurse Nat Void Nat (ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
Equal {a = Nat} {b = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} maximum 0 finalHistoryIn))) ([] {a = Void}) ([] {a = Nat}) No () Identity (MkMonad {m = Identity} {{conArg:9608} = MkApplicative {f = Identity} {{conArg:9127} = MkFunctor {f = Identity} (\0 b : Type,
0 a : Type,
func : a -> b,
{arg:8429} : Identity a =>
map {b} {a} func arg)} (\0 a : Type,
{arg:9131} : a =>
Id {a} arg) (\0 b : Type,
0 a : Type,
{arg:9137} : Identity (a -> b),
{arg:9144} : Identity a =>
<*> {b} {a} arg arg)} (\0 b : Type,
0 a : Type,
{arg:9612} : Identity a,
{arg:9615} : a -> Identity b =>
>>= {b} {a} arg arg) (\0 a : Type,
{arg:9626} : Identity (Identity a) =>
>>= {b = a} {a = Identity a} arg (id {a = Identity a}))) (Await {returnOut = Nat} {streamOut = Void} {streamIn = Nat} {returnInvariant = ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
Equal {a = Nat} {b = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} maximum 0 finalHistoryIn))} {streamInvariant = NoStreamInvariant {streamOut = Void} {streamIn = Nat}} {effects = Identity} {historyOut = [] {a = Void}} {historyIn = [] {a = Nat}} {returnIn = ()} (\returnValue : (),
0 {upstreamReturnProperty:5799} : Type,
0 returnProof : upstreamReturnProperty =>
Delay (Return {streamOut = Void} {streamIn = Nat} {streamInvariant = NoStreamInvariant {streamOut = Void} {streamIn = Nat}} {effects = Identity} {returnIn = ()} {historyOut = [] {a = Void}} {historyIn = [] {a = Nat}} {isInputExhausted = Yes upstreamReturnProperty returnProof} {returnOut = Nat} {returnInvariant = ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
=== {a = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} {t = List} {__con = Foldable implementation at Prelude.Types:428:1--441:59} maximum 0 finalHistoryIn))} 0 (Refl {a = Nat} {x = 0}))) (onStream Nat Nat 0 maximum 0 ([] {a = Nat}) (Refl {a = Nat} {x = 0}))) {innerReturnInvariant = ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
Equal {a = Nat} {b = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} maximum 0 finalHistoryIn))} {innerHistoryOut = [] {a = Void}} {innerHistoryIn = :: {a = Nat} value ([] {a = Nat})} {innerIsInputExhausted = No} (Delay (recurse Nat Nat 0 maximum (:: {a = Nat} value ([] {a = Nat})) (maximum value 0) (previousAccumulatorAppliedOnceEqualsNextFoldr Nat Nat 0 maximum 0 ([] {a = Nat}) (Refl {a = Nat} {x = 0}) value)))))))
in Element {type = returnOut} {pred = \returnValue : returnOut =>
returnInvariant (reverseOnto {a = streamIn} ([] {a = streamIn}) list) ([] {a = Void}) returnValue} returnValue (finalProof returnOut streamIn returnInvariant list pipe returnValue proofs originalResult))) (foldr {acc = Nat} {elem = Nat} maximum 0 (reverseOnto {a = Nat} ([] {a = Nat}) input)))
------------------------------
todo : ErasedThing (Equal {a = Nat} {b = Nat} (.fst {type = Nat} {pred = \returnValue : Nat =>
Equal {a = Nat} {b = Nat} returnValue (foldr {acc = Nat} {elem = Nat} maximum 0 (reverseOnto {a = Nat} ([] {a = Nat}) input))} (let Element {type = returnOut} {pred = \returnValue : returnOut =>
ComposedReturnProof {returnOut} {streamOut = Void} {streamIn = Void} {streamMid = streamIn} {returnMid = ()} (fromListReturnInvariant {streamOut = streamIn} list) (ExhaustsInputAnd {returnOut} {streamOut = Void} {streamIn} returnInvariant) (Yes () ()) ([] {a = Void}) ([] {a = Void}) returnValue} returnValue proofs =
.runIdentity {a = Subset Nat (\returnValue : Nat =>
ComposedReturnProof {returnOut = Nat} {streamOut = Void} {streamIn = Void} {streamMid = Nat} {returnMid = ()} (fromListReturnInvariant {streamOut = Nat} input) (ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} maxReturnInvariant) (Yes () ()) ([] {a = Void}) ([] {a = Void}) returnValue)} (runPipeWithInvariant {return = Nat} {returnInvariant = ComposedReturnProof {returnOut = Nat} {streamOut = Void} {streamIn = Void} {streamMid = Nat} {returnMid = ()} (fromListReturnInvariant {streamOut = Nat} input) (ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} maxReturnInvariant)} {effects = Identity} {{conArg:4374} = MkMonad {m = Identity} {{conArg:9608} = MkApplicative {f = Identity} {{conArg:9127} = MkFunctor {f = Identity} (\0 b : Type,
0 a : Type,
func : a -> b,
{arg:8429} : Identity a =>
map {b} {a} func arg)} (\0 a : Type,
{arg:9131} : a =>
Id {a} arg) (\0 b : Type,
0 a : Type,
{arg:9137} : Identity (a -> b),
{arg:9144} : Identity a =>
<*> {b} {a} arg arg)} (\0 b : Type,
0 a : Type,
{arg:9612} : Identity a,
{arg:9615} : a -> Identity b =>
>>= {b} {a} arg arg) (\0 a : Type,
{arg:9626} : Identity (Identity a) =>
>>= {b = a} {a = Identity a} arg (id {a = Identity a}))} (push Nat Void Nat (ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} maxReturnInvariant) (NoStreamInvariant {streamOut = Void} {streamIn = Nat}) ([] {a = Void}) () Void (fromListReturnInvariant {streamOut = Nat} input) (\currentHistoryIn : List Void,
currentHistoryOut : List Nat =>
DPair (List Nat) (\suffix : List Nat =>
Equal {a = List Nat} {b = List Nat} (++ {a = Nat} (reverseOnto {a = Nat} ([] {a = Nat}) currentHistoryOut) suffix) input)) ([] {a = Nat}) ([] {a = Void}) (Yes () ()) Void Identity (MkMonad {m = Identity} {{conArg:9608} = MkApplicative {f = Identity} {{conArg:9127} = MkFunctor {f = Identity} (\0 b : Type,
0 a : Type,
func : a -> b,
{arg:8429} : Identity a =>
map {b} {a} func arg)} (\0 a : Type,
{arg:9131} : a =>
Id {a} arg) (\0 b : Type,
0 a : Type,
{arg:9137} : Identity (a -> b),
{arg:9144} : Identity a =>
<*> {b} {a} arg arg)} (\0 b : Type,
0 a : Type,
{arg:9612} : Identity a,
{arg:9615} : a -> Identity b =>
>>= {b} {a} arg arg) (\0 a : Type,
{arg:9626} : Identity (Identity a) =>
>>= {b = a} {a = Identity a} arg (id {a = Identity a}))) {pushHistoryOut = [] {a = Void}} {effects' = Identity} {{conArg:3726} = MkMonad {m = Identity} {{conArg:9608} = MkApplicative {f = Identity} {{conArg:9127} = MkFunctor {f = Identity} (\0 b : Type,
0 a : Type,
func : a -> b,
{arg:8429} : Identity a =>
map {b} {a} func arg)} (\0 a : Type,
{arg:9131} : a =>
Id {a} arg) (\0 b : Type,
0 a : Type,
{arg:9137} : Identity (a -> b),
{arg:9144} : Identity a =>
<*> {b} {a} arg arg)} (\0 b : Type,
0 a : Type,
{arg:9612} : Identity a,
{arg:9615} : a -> Identity b =>
>>= {b} {a} arg arg) (\0 a : Type,
{arg:9626} : Identity (Identity a) =>
>>= {b = a} {a = Identity a} arg (id {a = Identity a}))} {pushIsInputExhaustedIn = Yes () ()} {pushHistoryIn = [] {a = Void}} {pushHistoryMid = [] {a = Nat}} (recurse Nat Identity (MkMonad {m = Identity} {{conArg:9608} = MkApplicative {f = Identity} {{conArg:9127} = MkFunctor {f = Identity} (\0 b : Type,
0 a : Type,
func : a -> b,
{arg:8429} : Identity a =>
map {b} {a} func arg)} (\0 a : Type,
{arg:9131} : a =>
Id {a} arg) (\0 b : Type,
0 a : Type,
{arg:9137} : Identity (a -> b),
{arg:9144} : Identity a =>
<*> {b} {a} arg arg)} (\0 b : Type,
0 a : Type,
{arg:9612} : Identity a,
{arg:9615} : a -> Identity b =>
>>= {b} {a} arg arg) (\0 a : Type,
{arg:9626} : Identity (Identity a) =>
>>= {b = a} {a = Identity a} arg (id {a = Identity a}))) input {{isInputExhausted:4695} = Yes () ()} {{historyIn:4694} = [] {a = Void}} {historyOut = [] {a = Nat}} input (Refl {a = List Nat} {x = input})) (\value : (),
0 {upstreamReturnProperty:1820} : Type,
0 upstreamReturnProof : upstreamReturnProperty =>
Delay (recurse Nat Void Nat (ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
Equal {a = Nat} {b = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} maximum 0 finalHistoryIn))) ([] {a = Void}) ([] {a = Nat}) No () Identity (MkMonad {m = Identity} {{conArg:9608} = MkApplicative {f = Identity} {{conArg:9127} = MkFunctor {f = Identity} (\0 b : Type,
0 a : Type,
func : a -> b,
{arg:8429} : Identity a =>
map {b} {a} func arg)} (\0 a : Type,
{arg:9131} : a =>
Id {a} arg) (\0 b : Type,
0 a : Type,
{arg:9137} : Identity (a -> b),
{arg:9144} : Identity a =>
<*> {b} {a} arg arg)} (\0 b : Type,
0 a : Type,
{arg:9612} : Identity a,
{arg:9615} : a -> Identity b =>
>>= {b} {a} arg arg) (\0 a : Type,
{arg:9626} : Identity (Identity a) =>
>>= {b = a} {a = Identity a} arg (id {a = Identity a}))) (Await {returnOut = Nat} {streamOut = Void} {streamIn = Nat} {returnInvariant = ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
Equal {a = Nat} {b = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} maximum 0 finalHistoryIn))} {streamInvariant = NoStreamInvariant {streamOut = Void} {streamIn = Nat}} {effects = Identity} {historyOut = [] {a = Void}} {historyIn = [] {a = Nat}} {returnIn = ()} (\returnValue : (),
0 {upstreamReturnProperty:5799} : Type,
0 returnProof : upstreamReturnProperty =>
Delay (Return {streamOut = Void} {streamIn = Nat} {streamInvariant = NoStreamInvariant {streamOut = Void} {streamIn = Nat}} {effects = Identity} {returnIn = ()} {historyOut = [] {a = Void}} {historyIn = [] {a = Nat}} {isInputExhausted = Yes upstreamReturnProperty returnProof} {returnOut = Nat} {returnInvariant = ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
=== {a = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} {t = List} {__con = Foldable implementation at Prelude.Types:428:1--441:59} maximum 0 finalHistoryIn))} 0 (Refl {a = Nat} {x = 0}))) (onStream Nat Nat 0 maximum 0 ([] {a = Nat}) (Refl {a = Nat} {x = 0}))) {innerReturnInvariant = ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
Equal {a = Nat} {b = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} maximum 0 finalHistoryIn))} {innerHistoryOut = [] {a = Void}} {innerHistoryIn = [] {a = Nat}} {innerIsInputExhausted = Yes upstreamReturnProperty upstreamReturnProof} (Delay (Return {streamOut = Void} {streamIn = Nat} {streamInvariant = NoStreamInvariant {streamOut = Void} {streamIn = Nat}} {effects = Identity} {returnIn = ()} {historyOut = [] {a = Void}} {historyIn = [] {a = Nat}} {isInputExhausted = Yes upstreamReturnProperty upstreamReturnProof} {returnOut = Nat} {returnInvariant = ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
=== {a = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} {t = List} {__con = Foldable implementation at Prelude.Types:428:1--441:59} maximum 0 finalHistoryIn))} 0 (Refl {a = Nat} {x = 0}))))) (\value : Nat =>
Delay (recurse Nat Void Nat (ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
Equal {a = Nat} {b = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} maximum 0 finalHistoryIn))) ([] {a = Void}) ([] {a = Nat}) No () Identity (MkMonad {m = Identity} {{conArg:9608} = MkApplicative {f = Identity} {{conArg:9127} = MkFunctor {f = Identity} (\0 b : Type,
0 a : Type,
func : a -> b,
{arg:8429} : Identity a =>
map {b} {a} func arg)} (\0 a : Type,
{arg:9131} : a =>
Id {a} arg) (\0 b : Type,
0 a : Type,
{arg:9137} : Identity (a -> b),
{arg:9144} : Identity a =>
<*> {b} {a} arg arg)} (\0 b : Type,
0 a : Type,
{arg:9612} : Identity a,
{arg:9615} : a -> Identity b =>
>>= {b} {a} arg arg) (\0 a : Type,
{arg:9626} : Identity (Identity a) =>
>>= {b = a} {a = Identity a} arg (id {a = Identity a}))) (Await {returnOut = Nat} {streamOut = Void} {streamIn = Nat} {returnInvariant = ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
Equal {a = Nat} {b = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} maximum 0 finalHistoryIn))} {streamInvariant = NoStreamInvariant {streamOut = Void} {streamIn = Nat}} {effects = Identity} {historyOut = [] {a = Void}} {historyIn = [] {a = Nat}} {returnIn = ()} (\returnValue : (),
0 {upstreamReturnProperty:5799} : Type,
0 returnProof : upstreamReturnProperty =>
Delay (Return {streamOut = Void} {streamIn = Nat} {streamInvariant = NoStreamInvariant {streamOut = Void} {streamIn = Nat}} {effects = Identity} {returnIn = ()} {historyOut = [] {a = Void}} {historyIn = [] {a = Nat}} {isInputExhausted = Yes upstreamReturnProperty returnProof} {returnOut = Nat} {returnInvariant = ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
=== {a = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} {t = List} {__con = Foldable implementation at Prelude.Types:428:1--441:59} maximum 0 finalHistoryIn))} 0 (Refl {a = Nat} {x = 0}))) (onStream Nat Nat 0 maximum 0 ([] {a = Nat}) (Refl {a = Nat} {x = 0}))) {innerReturnInvariant = ExhaustsInputAnd {returnOut = Nat} {streamOut = Void} {streamIn = Nat} (\finalHistoryIn : List Nat,
finalHistoryOut : List Void,
finalReturn : Nat =>
Equal {a = Nat} {b = Nat} finalReturn (foldr {acc = Nat} {elem = Nat} maximum 0 finalHistoryIn))} {innerHistoryOut = [] {a = Void}} {innerHistoryIn = :: {a = Nat} value ([] {a = Nat})} {innerIsInputExhausted = No} (Delay (recurse Nat Nat 0 maximum (:: {a = Nat} value ([] {a = Nat})) (maximum value 0) (previousAccumulatorAppliedOnceEqualsNextFoldr Nat Nat 0 maximum 0 ([] {a = Nat}) (Refl {a = Nat} {x = 0}) value)))))))
in Element {type = returnOut} {pred = \returnValue : returnOut =>
returnInvariant (reverseOnto {a = streamIn} ([] {a = streamIn}) list) ([] {a = Void}) returnValue} returnValue (finalProof returnOut streamIn returnInvariant list pipe returnValue proofs originalResult))) (foldr {acc = Nat} {elem = Nat} maximum 0 (reverseOnto {a = Nat} ([] {a = Nat}) input)))
Created
December 12, 2022 06:51
-
-
Save ErnWong/f107e4b73ede1a4be47f359555f12074 to your computer and use it in GitHub Desktop.
Thicc Idris Types
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment