builtin field axiom Field : TypeSource#

builtin field-add axiom + : Field -> Field -> FieldSource#

builtin field-sub axiom - : Field -> Field -> FieldSource#

builtin field-mul axiom * : Field -> Field -> FieldSource#

builtin field-div axiom / : Field -> Field -> FieldSource#

builtin field-eq axiom == : Field -> Field -> BoolSource#

builtin field-from-int axiom fromInt : Int -> FieldSource#

builtin field-to-nat axiom toNat : Field -> NatSource#

fromNat (n : Nat) : FieldSource#

toInt (f : Field) : IntSource#