Commit e8e36fb7 authored by Sven Wille's avatar Sven Wille

finsequences foldr error

parent 61a54382
......@@ -37,11 +37,13 @@ theory FinSeqFunctions : base:?InductiveTypes =
finiteSequenceMap : {A : type} {B : type} {n : INat} finSeq n A ⟶ (A ⟶ B) ⟶ finSeq n B ❘= [A , B , n , fn , mp] [a ,b ,c] mp (fn a b c) ❘ # finSeqMap 4 5 ❙
def finiteSequenceFoldR (A : type , B : type , fn : A ⟶ B ⟶ B ) ❘ =
finSeqFoldR : {n : INat }{m : INat } B ⟶ ⊦ leN n m ⟶ finSeq n A ⟶ B ❙
def finiteSequenceFoldR (A : type , B : type , startValue : B , fn : A ⟶ B ⟶ B , n : INat, fs : finSeq n A ) ❘ =
finSeqFoldR : {m : INat } ⊦ leN m n ⟶ B ❙
// Zero = [p : ⊦ leN Zero n] startValue ❙
// Suc = [mm][p : ⊦ leN (Suc mm) n] startValue ❙
// Zero = [A : type][B : type][n : INat][startValue : B][p : ⊦ leN Zero n][fs : finSeq n A][fn : A ⟶ B ⟶ B] startValue ❙
// Suc = [m : INat][A : type][B : type][n : INat][startValue : B][p : ⊦ leN Zero n][fs : finSeq n A][fn : A ⟶ B ⟶ B] startValue ❙
// Zero = [A : type][B : type][n : INat][startValue : B][p : ⊦ leN Zero n][fs : finSeq n A][fn : A ⟶ B ⟶ B] startValue ❙
// Suc = [m : INat][A : type][B : type][n : INat][startValue : B][p : ⊦ leN Zero n][fs : finSeq n A][fn : A ⟶ B ⟶ B] startValue ❙
// Suc = [m][A][B][n][startValue][h][fs][fn] fn (fs (Suc m) (lemma_One_le_Suc m) h) startValue ❙
// bla : {A : type} {n : INat} {m : INat} ⊦ leN (Suc Zero ) m ⟶ ⊦ leN m n ⟶ finSeq n A ⟶ A ❘ = [A , n , m , p , p0 , fs] fs m p p0 ❙
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment