List sorts.
Definition at line 25 of file ListSort.java.
◆ getConsDecl()
The declaration of the cons function of this list sort.
- Exceptions
-
Definition at line 58 of file ListSort.java.
60 return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
◆ getHeadDecl()
The declaration of the head function of this list sort.
- Exceptions
-
Definition at line 77 of file ListSort.java.
79 return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
◆ getIsConsDecl()
The declaration of the isCons function of this list sort.
- Exceptions
-
Definition at line 68 of file ListSort.java.
70 return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
◆ getIsNilDecl()
The declaration of the isNil function of this list sort.
- Exceptions
-
Definition at line 49 of file ListSort.java.
51 return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
◆ getNil()
◆ getNilDecl()
The declaration of the nil function of this list sort.
- Exceptions
-
Definition at line 31 of file ListSort.java.
33 return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
Referenced by ListSort.getNil().
◆ getTailDecl()
The declaration of the tail function of this list sort.
- Exceptions
-
Definition at line 86 of file ListSort.java.
88 return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1));
Expr mkApp(FuncDecl f, Expr... args)