blob: a361e24fdd862f92ef5bfc4f4dc1eb394b754d14 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Require Import Coq.ZArith.BinInt.
Require Import Crypto.Compilers.Wf.
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.GeneralizeVarInterp.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.Z.GeneralizeVar.
Definition InterpGeneralizeVar
{interp_base_type}
{interp_op}
{t} (e : Expr t)
(Hwf : Wf e)
e'
(He' : GeneralizeVar (e _) = Some e')
: forall v, Compilers.Syntax.Interp (interp_base_type:=interp_base_type) interp_op e' v
= Compilers.Syntax.Interp interp_op e v
:= @InterpGeneralizeVar
base_type op base_type_beq internal_base_type_dec_bl
internal_base_type_dec_lb
(fun _ t => Op (OpConst 0%Z) TT)
interp_base_type
interp_op
t e Hwf e' He'.
|
