module char where open import bool open import nat open import eq open import product open import product-thms ---------------------------------------------------------------------- -- datatypes ---------------------------------------------------------------------- postulate char : Set {-# BUILTIN CHAR char #-} ---------------------------------------------------------------------- -- primitive operations ---------------------------------------------------------------------- private primitive primCharToNat : char β†’ β„• primCharEquality : char β†’ char β†’ 𝔹 toNat : char β†’ β„• toNat = primCharToNat infix 4 _=char_ _=char_ : char β†’ char β†’ 𝔹 _=char_ = primCharEquality postulate ≑char-to-= : (c1 c2 : char) β†’ c1 ≑ c2 β†’ _=char_ c1 c2 ≑ tt =char-to-≑ : (c1 c2 : char) β†’ _=char_ c1 c2 ≑ tt β†’ c1 ≑ c2 =char-sym : (c1 c2 : char) β†’ (c1 =char c2) ≑ (c2 =char c1) =char-sym c1 c2 with keep (c1 =char c2) =char-sym c1 c2 | tt , p rewrite =char-to-≑ c1 c2 p = refl =char-sym c1 c2 | ff , p with keep (c2 =char c1) =char-sym c1 c2 | ff , p | tt , p' rewrite =char-to-≑ c2 c1 p' = refl =char-sym c1 c2 | ff , p | ff , p' rewrite p | p' = refl postulate _