<commit_before>------------------------------------------------------------------------------
-- Sort a list
------------------------------------------------------------------------------

-- This module define the program which sorts a list by converting it
-- into an ordered tree and then back to a list (Burstall, 1969, pp. 45).

-- <NAME>. Proving properties of programs by structural
-- induction. The Computer Journal, 12(1):41–48, 1969.

module Examples.SortList.SortList where

open import LTC.Minimal

open import LTC.Data.Bool
open import LTC.Data.Nat
open import LTC.Data.Nat.Inequalities
open import LTC.Data.List

------------------------------------------------------------------------------
-- Tree terms
postulate
  nilTree  : D
  tip      : D → D
  node     : D → D → D → D

-- The LTC tree data type
data Tree : D → Set where
  nilT  : Tree nilTree
  tipT  : {i : D} → N i → Tree (tip i)
  nodeT : {t₁ i t₂ : D} → Tree t₁ → N i → Tree t₂ → Tree (node t₁ i t₂)
{-# ATP hint nilT #-}
{-# ATP hint tipT #-}<commit_msg>Added missing page.<commit_after>------------------------------------------------------------------------------
-- Sort a list
------------------------------------------------------------------------------

-- This module define the program which sorts a list by converting it
-- into an ordered tree and then back to a list (Burstall, 1969, pp. 45-46).

-- <NAME>. Proving properties of programs by structural
-- induction. The Computer Journal, 12(1):41–48, 1969.

module Examples.SortList.SortList where

open import LTC.Minimal

open import LTC.Data.Bool
open import LTC.Data.Nat
open import LTC.Data.Nat.Inequalities
open import LTC.Data.List

------------------------------------------------------------------------------
-- Tree terms
postulate
  nilTree  : D
  tip      : D → D
  node     : D → D → D → D

-- The LTC tree data type
data Tree : D → Set where
  nilT  : Tree nilTree
  tipT  : {i : D} → N i → Tree (tip i)
  nodeT : {t₁ i t₂ : D} → Tree t₁ → N i → Tree t₂ → Tree (node t₁ i t₂)
{-# ATP hint nilT #-}
{-# ATP hint tipT #-}
{'fraction_non_alphanumeric': 0.30909966297544533, 'fraction_numerical': 0.017332691381800675, 'mean_word_length': 1.3012181616832779, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, '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': '6695131', 'n_tokens_mistral': 616, 'n_tokens_neox': 583, 'n_words': 258}