Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Infered

Agda.Utils.Size

# Documentation

class Sized a where

Methods

size :: Integral n => a -> n

Instances

Sized Permutation |
Sized ModuleName |
Sized QName |
Sized LevelAtom |
Sized PlusLevel |
Sized Level |
Sized Type |
Sized Term |
Sized Substitution |
Sized [a] |
Sized a => Sized (Maybe a) |
Sized (Set a) |
Sized a => Sized (Arg a) |
Sized a => Sized (Dom a) |
Sized (Tele a) |
Sized a => Sized (Abs a) |
Sized (Map k a) |
Sized a => Sized (Named name a) |