Description

Definitions

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