UniAgda.Core.Types.Unit

Table of Contents

1 Prelude

2 Unit Type

The unit type is an inductive type with only one term defined.

data Unit : Type lzero where
  tt : Unit

Author: James Leslie

Created: 2021-03-27 Sat 10:47