blob: 32b84aa1f0f0673a2cc185a6e826858daa8529d2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Wf.
Require Import Crypto.Compilers.InlineWf.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.Z.Inline.
Definition Wf_InlineConst {t} (e : Expr base_type op t) (Hwf : Wf e)
: Wf (InlineConst e)
:= @Wf_InlineConst _ _ _ t e Hwf.
Hint Resolve Wf_InlineConst : wf.
|
