nspec - 0.1.1

Juvix.Builtin.V1.Trait.Natural

Description

Definitions

trait type Natural ASource#

Constructors

| mkNatural@{ {{FromNaturalI}} : FromNatural A; syntax operator + additive; {-# isabelle-operator: {name: "+", prec: 65, assoc: left} #-} + : A -> A -> A; syntax operator * multiplicative; {-# isabelle-operator: {name: "*", prec: 70, assoc: left} #-} * : A -> A -> A; }

open Natural public