Full sequence.
(s: SortRef)
| 3932 | |
| 3933 | |
| 3934 | def Full(s: SortRef) -> ExprRef: |
| 3935 | """Full sequence.""" |
| 3936 | if isinstance(s, ArraySortRef): |
| 3937 | return FullSet(s.domain()) |
| 3938 | raise NotImplementedError("Full not supported for this sort") |
| 3939 | |
| 3940 | |
| 3941 | def Unit(e: ExprRef) -> ExprRef: |