blob: bc3c8f6a90efb96d4b2bfb649a641eb0802c84c2 (
plain)
1
2
3
4
5
6
7
8
9
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.Z.Syntax.Util.
Require Import Crypto.Compilers.InterpSideConditions.
Require Import Crypto.Util.PointedProp.
Require Import Crypto.Util.Notations.
Definition InterpSideConditions {t} (e : Expr t) : interp_flat_type interp_base_type (domain t) -> pointed_Prop
:= InterpSideConditions interp_op (@interped_op_side_conditions) e.
|
