Tuples, sort-erased

mkTuple builds a tuple, tupleSelect (with fst and snd) reads one component, and tupleProject answers a tuple of the components selected: projecting a single index gives a one-component tuple, not that component.

def Cvc.Untyped.Term.mkTuple [Ω] (terms : Terms) : Env Term

The tuple whose components are the given terms, in order.

Equations

• Cvc.Untyped.Term.mkTuple terms = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTuple terms

def Cvc.Untyped.Term.tupleProject [Ω] (indices : Array Nat) (tuple : Term) : Env Term

The tuple of the components at the given indices, in the order given.

Indices count from zero. They need be neither increasing nor distinct, so this reorders and duplicates as well as it selects: projecting #[2, 0] out of (Tuple Int Bool Real) gives (Tuple Real Int).

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Untyped.Term.tupleSelect [Ω] (idx : Nat) (tuple : Term) : Env Term

The component at the given index, at that component's own sort.

Unlike tupleProject #[1], which answers (Tuple Bool) on a (Tuple Int Bool String), this answers Bool.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Cvc.Untyped.Term.fst [Ω] (t : Term) : Env Term

A tuple's first component.

Equations

• t.fst = Cvc.Untyped.Term.tupleSelect 0 t

@[reducible, inline]

abbrev Cvc.Untyped.Term.snd [Ω] (t : Term) : Env Term

A tuple's second component.

Equations

• t.snd = Cvc.Untyped.Term.tupleSelect 1 t

Values

def Cvc.Untyped.Term.isTupleValue [Ω] (term : Term) : Bool

Determine if this term is a tuple value.

Equations

• term.isTupleValue = (Cvc.Untyped.Term.toUnsafe✝ term).isTupleValue

def Cvc.Untyped.Term.getTupleValue [Ω] (term : Term) : Res Terms

The components a constant tuple term denotes, failing if it denotes none.

Equations

• term.getTupleValue = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Untyped.Term.toUnsafe✝ term).getTupleValue

class Cvc.Untyped.Term.TupleTail (β : Type) : Type 1

How the last component of a product converts: a product there flattens into the tuple.

α × β × γ is one tuple of three components, so converting α × β expands β when it is itself a product (or a OneTuple), and takes it as one component otherwise.

• toTerms [Ω] : β → Env (List Term)

  The terms of the components b stands for.

• ofTerms [Ω] : List Term → Env β

  Reads a value off the remaining components, all of them.

@[instance_reducible, instance 100]

instance Cvc.Untyped.Term.instTupleTailOfToTypOfValueToTermOfTermToValue {β : Type} [ToTyp β] [ValueToTerm β] [TermToValue β] : TupleTail β

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Cvc.Untyped.Term.instTupleTailProdOfValueToTermOfTermToValue {α β : Type} [ValueToTerm α] [TermToValue α] [TupleTail β] : TupleTail (α × β)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Cvc.Untyped.Term.instTupleTailOneTupleOfValueToTermOfTermToValue {α : Type} [ValueToTerm α] [TermToValue α] : TupleTail (OneTuple α)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Cvc.Untyped.Term.instValueToTermProdOfTupleTail {α β : Type} [ValueToTerm α] [TupleTail β] : ValueToTerm (α × β)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Cvc.Untyped.Term.instTermToValueProdOfTupleTail {α β : Type} [TermToValue α] [TupleTail β] : TermToValue (α × β)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Cvc.Untyped.Term.instValueToTermOneTuple {α : Type} [ValueToTerm α] : ValueToTerm (OneTuple α)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Cvc.Untyped.Term.instTermToValueOneTuple {α : Type} [TermToValue α] : TermToValue (OneTuple α)

Equations

• One or more equations did not get rendered due to their size.