import { Goal } from "../goal";
export declare type Value = PatternVar | String | Number | Boolean | Null | ListCons | ListNull | Objekt | Relation;
export declare type PatternVar = {
    family: "Value";
    kind: "PatternVar";
    name: string;
};
export declare function PatternVar(name: string): PatternVar;
export declare type String = {
    family: "Value";
    kind: "String";
    data: string;
};
export declare function String(data: string): String;
export declare type Number = {
    family: "Value";
    kind: "Number";
    data: number;
};
export declare function Number(data: number): Number;
export declare type Boolean = {
    family: "Value";
    kind: "Boolean";
    data: boolean;
};
export declare function Boolean(data: boolean): Boolean;
export declare type Null = {
    family: "Value";
    kind: "Null";
};
export declare function Null(): Null;
export declare type ListCons = {
    family: "Value";
    kind: "ListCons";
    car: Value;
    cdr: Value;
};
export declare function ListCons(car: Value, cdr: Value): ListCons;
export declare type ListNull = {
    family: "Value";
    kind: "ListNull";
};
export declare function ListNull(): ListNull;
export declare type Objekt = {
    family: "Value";
    kind: "Objekt";
    properties: Record<string, Value>;
};
export declare function Objekt(properties: Record<string, Value>): Objekt;
export declare type Relation = {
    family: "Value";
    kind: "Relation";
    clauses: Array<Clause>;
};
export declare function Relation(clauses: Array<Clause>): Relation;
/**

   ## Named clauses

   A clause has a name -- written after the line.

   With named clauses, we can write proofs by hand,
   just like writing inductive datatype in dependent type.

**/
export declare type Clause = {
    name: string;
    value: Value;
    goals: Array<Goal>;
};
export declare function Clause(name: string, value: Value, goals: Array<Goal>): Clause;