import { GlobalEnv } from "./globalenv";
import { Env, Synthed } from "./types";
import * as ast from "../ast";
export declare type mode = null | {
    tag: "@requires";
} | {
    tag: "@ensures";
    returns: ast.Type;
} | {
    tag: "@loop_invariant";
} | {
    tag: "@assert";
};
/** Asserts that a synthesized type has small type */
export declare function synthLValue(genv: GlobalEnv, env: Env, mode: mode, exp: ast.LValue): ast.ValueType;
export declare function synthExpression(genv: GlobalEnv, env: Env, mode: mode, exp: ast.Expression): Synthed;
export declare function checkExpression(genv: GlobalEnv, env: Env, mode: mode, exp: ast.Expression, tp: ast.Type): void;