view work.agda~ @ 825:02f431665ebc

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 29 Jan 2024 11:42:39 +0900
parents 68904fdaab71
children
line wrap: on
line source

module work where

open import Level hiding (suc ; zero ; _⊔_ )

open import Data.Nat hiding (compare)
open import Data.Nat.Properties as NatProp
open import Data.Maybe
-- open import Data.Maybe.Properties
open import Data.Empty
open import Data.List
open import Data.Product

open import Function as F hiding (const)

open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import logic

data bt {n : Level} (A : Set n) : Set n where
  leaf : bt A
  node : (key : ℕ) → (value : A) → (left : bt A) → (right : bt A) → bt A