<commit_before>------------------------------------------------------------------------------
-- The FOTC stream type
------------------------------------------------------------------------------

{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K #-}

module FOTC.Data.Stream.Type where

open import FOTC.Base

------------------------------------------------------------------------------
-- Functional for the FOTC Stream type.
-- StreamF : (D → Set) → D → Set
-- StreamF P ds = ∃[ e ] ∃[ es ] P es ∧ ds ≡ e ∷ es

-- Stream is the greatest fixed-point of StreamF (by Stream-gfp₁ and
-- Stream-gfp₂).

postulate
  Stream : D → Set

postulate
-- Stream is a post-fixed point of StreamF, i.e.
--
-- Stream ≤ StreamF Stream.
  Stream-gfp₁ : ∀ {xs} → Stream xs →
                ∃[ x' ] ∃[ xs' ] Stream xs' ∧ xs ≡ x' ∷ xs'
{-# ATP axiom Stream-gfp₁ #-}

-- Stream is the greatest post-fixed point of StreamF, i.e
--
-- ∀ P. P ≤ StreamF P ⇒ P ≤ Stream.
--
-- N.B. This is an axiom schema. Because in the automatic proofs we
-- *must* use an instance, we do not add this postulate as an ATP
-- axiom.
postulate
  Stream-gfp₂ : (P : D → Set) →
                -- P is post-fixed point of StreamF.
                (∀ {xs} → P xs → ∃[ x' ] ∃[ xs' ] P xs' ∧ xs ≡ x' ∷ xs') →
                -- Stream is greater than P.<commit_msg>Cosmetic change.<commit_after>------------------------------------------------------------------------------
-- The FOTC stream type
------------------------------------------------------------------------------

{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K #-}

module FOTC.Data.Stream.Type where

open import FOTC.Base

------------------------------------------------------------------------------
-- Functional for the FOTC Stream type.
-- StreamF : (D → Set) → D → Set
-- StreamF P xs = ∃[ x' ] ∃[ xs' ] P xs' ∧ xs ≡ x' ∷ xs'

-- Stream is the greatest fixed-point of StreamF (by Stream-gfp₁ and
-- Stream-gfp₂).

postulate
  Stream : D → Set

postulate
-- Stream is a post-fixed point of StreamF, i.e.
--
-- Stream ≤ StreamF Stream.
  Stream-gfp₁ : ∀ {xs} → Stream xs →
                ∃[ x' ] ∃[ xs' ] Stream xs' ∧ xs ≡ x' ∷ xs'
{-# ATP axiom Stream-gfp₁ #-}

-- Stream is the greatest post-fixed point of StreamF, i.e
--
-- ∀ P. P ≤ StreamF P ⇒ P ≤ Stream.
--
-- N.B. This is an axiom schema. Because in the automatic proofs we
-- *must* use an instance, we do not add this postulate as an ATP
-- axiom.
postulate
  Stream-gfp₂ : (P : D → Set) →
                -- P is post-fixed point of StreamF.
                (∀ {xs} → P xs → ∃[ x' ] ∃[ xs' ] P xs' ∧ xs ≡ x' ∷ xs') →
                -- Stream is greater than P.
{'fraction_non_alphanumeric': 0.3020833333333333, 'fraction_numerical': 0.0, 'mean_word_length': 1.227837613918807, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4987044', 'n_tokens_mistral': 959, 'n_tokens_neox': 855, 'n_words': 354}