view work.agda~ @ 842:ee2dd920e414

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 21 Mar 2024 15:25:37 +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