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

Safe HaskellSafe-Inferred

Agda.Utils.Size

Documentation

class Sized a whereSource

Methods

size :: Integral n => a -> nSource

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 (Tele a) 
Sized a => Sized (Abs a) 
Sized a => Sized (Elim' a) 
Sized (Map k a) 
Sized a => Sized (Named name a) 
Sized a => Sized (Dom c a) 
Sized a => Sized (Arg c a)