import type { Closure } from "../closure/index.js";
import type { Neutral } from "../neutral/index.js";
import * as Neutrals from "../neutral/index.js";
export type Value = TypedNeutral | Type | Pi | PiImplicit | Fn | FnImplicit | Sigma | Cons | String | Quote | Trivial | Sole | Clazz | Objekt | Equal | Refl;
export type AlreadyType = Type | Pi | PiImplicit | Sigma | String | Trivial | Clazz | Equal;
export type PatternVar = TypedNeutral & {
    neutral: Neutrals.PatternVar;
};
export declare function PatternVar(type: Value, name: string): PatternVar;
export declare function isPatternVar(value: Value): value is PatternVar;
export type TypedNeutral = {
    "@type": "Value";
    "@kind": "TypedNeutral";
    type: Value;
    neutral: Neutral;
};
export declare function TypedNeutral(type: Value, neutral: Neutral): TypedNeutral;
export type Type = {
    "@type": "Value";
    "@kind": "Type";
};
export declare function Type(): Type;
export type Pi = {
    "@type": "Value";
    "@kind": "Pi";
    argType: Value;
    retTypeClosure: Closure;
};
export declare function Pi(argType: Value, retTypeClosure: Closure): Pi;
export type PiImplicit = {
    "@type": "Value";
    "@kind": "PiImplicit";
    argType: Value;
    retTypeClosure: Closure;
};
export declare function PiImplicit(argType: Value, retTypeClosure: Closure): PiImplicit;
export type Fn = {
    "@type": "Value";
    "@kind": "Fn";
    retClosure: Closure;
};
export declare function Fn(retClosure: Closure): Fn;
export type FnImplicit = {
    "@type": "Value";
    "@kind": "FnImplicit";
    retClosure: Closure;
};
export declare function FnImplicit(retClosure: Closure): FnImplicit;
export type Sigma = {
    "@type": "Value";
    "@kind": "Sigma";
    carType: Value;
    cdrTypeClosure: Closure;
};
export declare function Sigma(carType: Value, cdrTypeClosure: Closure): Sigma;
export type Cons = {
    "@type": "Value";
    "@kind": "Cons";
    car: Value;
    cdr: Value;
};
export declare function Cons(car: Value, cdr: Value): Cons;
export type String = {
    "@type": "Value";
    "@kind": "String";
};
export declare function String(): String;
export type Quote = {
    "@type": "Value";
    "@kind": "Quote";
    data: string;
};
export declare function Quote(data: string): Quote;
export type Trivial = {
    "@type": "Value";
    "@kind": "Trivial";
};
export declare function Trivial(): Trivial;
export type Sole = {
    "@type": "Value";
    "@kind": "Sole";
};
export declare function Sole(): Sole;
export type Clazz = ClazzNull | ClazzCons | ClazzFulfilled;
export type ClazzNull = {
    "@type": "Value";
    "@kind": "ClazzNull";
    name?: string;
};
export declare function ClazzNull(name?: string): ClazzNull;
export type ClazzCons = {
    "@type": "Value";
    "@kind": "ClazzCons";
    propertyName: string;
    propertyType: Value;
    restClosure: Closure;
    name?: string;
};
export declare function ClazzCons(propertyName: string, propertyType: Value, restClosure: Closure, name?: string): ClazzCons;
export type ClazzFulfilled = {
    "@type": "Value";
    "@kind": "ClazzFulfilled";
    propertyName: string;
    propertyType: Value;
    property: Value;
    rest: Clazz;
    name?: string;
};
export declare function ClazzFulfilled(propertyName: string, propertyType: Value, property: Value, rest: Clazz, name?: string): ClazzFulfilled;
export type Objekt = {
    "@type": "Value";
    "@kind": "Objekt";
    properties: Record<string, Value>;
};
export declare function Objekt(properties: Record<string, Value>): Objekt;
export type Equal = {
    "@type": "Value";
    "@kind": "Equal";
    type: Value;
    from: Value;
    to: Value;
};
export declare function Equal(type: Value, from: Value, to: Value): Equal;
export type Refl = {
    "@type": "Value";
    "@kind": "Refl";
    type: Value;
    value: Value;
};
export declare function Refl(type: Value, value: Value): Refl;
//# sourceMappingURL=Value.d.ts.map