MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / Nat

Function Nat

lean_py/z3/core.py:1062–1064  ·  view source on GitHub ↗
(name: str)

Source from the content-addressed store, hash-verified

1060
1061
1062def Nat(name: str) -> ArithRef:
1063 s = NatSort()
1064 return ArithRef(_AstVar(name), s, frozenset([(name, s._ast_sort)]))
1065
1066
1067def Real(name: str) -> ArithRef:

Callers 12

test_forall_nat_succMethod · 0.90
test_prove_nat_nonnegMethod · 0.90
test_is_arithMethod · 0.90
test_nat_varMethod · 0.90
test_nat_identityMethod · 0.90
test_nat_arithMethod · 0.90
test_nat_nonnegMethod · 0.90
test_nat_succ_posMethod · 0.90
test_nat_nonnegMethod · 0.90
test_square_nonnegMethod · 0.90
test_nat_has_predecessorMethod · 0.90
nat_arithmeticFunction · 0.85

Calls 2

NatSortFunction · 0.85
ArithRefClass · 0.85

Tested by 11

test_forall_nat_succMethod · 0.72
test_prove_nat_nonnegMethod · 0.72
test_is_arithMethod · 0.72
test_nat_varMethod · 0.72
test_nat_identityMethod · 0.72
test_nat_arithMethod · 0.72
test_nat_nonnegMethod · 0.72
test_nat_succ_posMethod · 0.72
test_nat_nonnegMethod · 0.72
test_square_nonnegMethod · 0.72
test_nat_has_predecessorMethod · 0.72