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

Function FreshConst

lean_py/z3/core.py:2151–2155  ·  view source on GitHub ↗

Create a fresh constant with a unique name.

(sort: SortRef, prefix: str = "c")

Source from the content-addressed store, hash-verified

2149
2150
2151def FreshConst(sort: SortRef, prefix: str = "c") -> ExprRef:
2152 """Create a fresh constant with a unique name."""
2153 global _fresh_counter
2154 _fresh_counter += 1
2155 return Const(f"{prefix}!{_fresh_counter}", sort)
2156
2157
2158def FreshInt(prefix: str = "x") -> ArithRef:

Callers 6

FreshIntFunction · 0.85
FreshBoolFunction · 0.85
FreshRealFunction · 0.85

Calls 1

ConstFunction · 0.85

Tested by 3