mk
open fun <D : KSort, R : KSort> mkArrayLambda(indexVar: KDecl<D>, body: KExpr<R>): KArrayLambda<D, R>
Create an array lambda expression (lambda (indexVar) body).
The sort of the lambda expression is an array where the domain is the array are the indexVar sort and the range is the sort of the body of the lambda expression.
If (= L (lambda (i D)) (body i)) then (forall (i D) (= (select L i) (body i))).
open fun <D0 : KSort, D1 : KSort, R : KSort> mkArrayLambda(indexVar0: KDecl<D0>, indexVar1: KDecl<D1>, body: KExpr<R>): KArray2Lambda<D0, D1, R>
Create an array lambda expression (lambda (indexVar0) body).
See also
open fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArrayLambda(indexVar0: KDecl<D0>, indexVar1: KDecl<D1>, indexVar2: KDecl<D2>, body: KExpr<R>): KArray3Lambda<D0, D1, D2, R>
Create an array lambda expression (lambda (indexVar0 indexVar2) body).