docs - 0.0.0

Stdlib.Trait.Integral

Description

Definitions

trait type Integral ASource#

Constructors

| mkIntegral { naturalI : Natural A; syntax operator - additive; {-# isabelle-operator: {name: "-", prec: 65, assoc: left} #-} - : A -> A -> A; builtin from-int fromInt : Int -> A }

open Integral using {fromInt; -} public