📥 Download raw
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProvingBasics.Connectives.Disjunction

module Padova2025.VerifiedAlgorithms.InsertionSort.Implementation
  (A : Set) (_≤_ : A → A → Set) (cmp? : (x y : A) → x ≤ y ⊎ y ≤ x) where

Implementation

Explanation

Contract: “insert x ys” is ascendingly ordered, if “ys” is ascendingly ordered.

insert : A → List A → List A
insert = {!!}

sort : List A → List A
sort = {!!}