blob: 7429eaba7f3e6f5515de6f078df6f8bef8187887 (
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 base_type op t) : interp_flat_type interp_base_type (domain t) -> pointed_Prop
:= InterpSideConditions interp_op (@interped_op_side_conditions) e.
|
