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

Function NatVal

lean_py/z3/core.py:1139–1140  ·  view source on GitHub ↗
(n: int)

Source from the content-addressed store, hash-verified

1137
1138
1139def NatVal(n: int) -> IntNumRef:
1140 return IntNumRef(NatLit(n), NatSort())
1141
1142
1143def RealVal(n: int | float | str) -> ArithRef:

Callers 9

test_natvalMethod · 0.90
test_natval_returns_intnumrefMethod · 0.90
test_val_constructorsMethod · 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
test_nat_induction_baseMethod · 0.90

Calls 3

NatLitClass · 0.90
IntNumRefClass · 0.85
NatSortFunction · 0.85

Tested by 9

test_natvalMethod · 0.72
test_natval_returns_intnumrefMethod · 0.72
test_val_constructorsMethod · 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
test_nat_induction_baseMethod · 0.72