Commit 2ed06e52 authored by Sven Wille's avatar Sven Wille

finsequences foldr

parent d945934b
......@@ -158,3 +158,11 @@ theory NatConversions : base:?InductiveTypes =
theory INatProps : base:?Logic =
include ?INatArith ❙
lemma_Zero_lt_Suc : {m : INat} ⊦ ltN Zero (Suc m) ❙
lemma_Zero_le_Suc : {m : INat} ⊦ leN Zero (Suc m) ❙
lemma_One_le_Suc : {m : INat} ⊦ ltN (Suc Zero) (Suc m) ❙
......@@ -26,19 +26,21 @@ theory FinSeqProps : base:?InductiveTypes =
def strictly_ascending_rec () ❘ =
strictly_asc_rec : {m : INat}{n : INat} finSeq n ℝ ⟶ bool ❘ # strictAscRec 1 3 ❙
strictly_asc_rec : {m : INat}{n : INat} finSeq n ℝ ⟶ bool ❘ # strictAscRec 1 3 ❙ // sw : ignore this function for the time beeing ! ❙
theory FinSeqFunctions : base:?Logic =
include ?FinSequences ❙
include arith:?INatProps❙
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 finiteSequenceFoldL : (A : type , B : type , fn : A ⟶ B ⟶ A , starValue : A ) ❘ =
finSeqFoldL : {n : INat } ⟶ finSeq n B ⟶ A❙
Zero ❙
def finiteSequenceFoldL : (A : type , B : type , fn : A ⟶ B ⟶ A , starValue : A, n : INat ) ❘ =
finSeqFoldR : {m : INat } ⊦ leN m n ⟶ finSeq n B ⟶ A❙
Zero = [h][fs] startValue ❙
Suc = [m][h][fs] fs (Suc m) (lemma_one_le_Suc (Suc m)) h finSeqFoldR m fs❙
......
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