view work.agda~ @ 793:08e04ed15468

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 21 Oct 2023 18:51:25 +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