SMT array sort, maps to Lean function type ``dom → rng``.
| 254 | |
| 255 | |
| 256 | class ArraySortRef(SortRef): |
| 257 | """SMT array sort, maps to Lean function type ``dom → rng``.""" |
| 258 | |
| 259 | __slots__ = ("_domain", "_range") |
| 260 | |
| 261 | def __init__(self, domain: SortRef, range_sort: SortRef) -> None: |
| 262 | super().__init__(ArrowASTSort(domain._ast_sort, range_sort._ast_sort)) |
| 263 | self._domain = domain |
| 264 | self._range = range_sort |
| 265 | |
| 266 | def domain(self) -> SortRef: |
| 267 | return self._domain |
| 268 | |
| 269 | def range(self) -> SortRef: |
| 270 | return self._range |
| 271 | |
| 272 | |
| 273 | def ArraySort(domain: SortRef, range_sort: SortRef) -> ArraySortRef: |
no outgoing calls
no test coverage detected