blob: 3cacf7a1bc4bf25e8bd546d7df47a2af0a796f27 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.SmartMap.
Require Import Crypto.Reflection.Named.Syntax.
Module Export Named.
Section language.
Context {base_type_code : Type}
{interp_base_type : base_type_code -> Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}
{Name : Type}.
(** [SmartVar] is like [Var], except that it inserts
pair-projections and [Pair] as necessary to handle
[flat_type], and not just [base_type_code] *)
Definition SmartVar {t} : interp_flat_type (fun _ => Name) t -> @exprf base_type_code op Name t
:= smart_interp_flat_map (f:=fun _ => Name) (g:=@exprf _ _ _) (fun t => Var) TT (fun A B x y => Pair x y).
End language.
End Named.
Global Arguments SmartVar {_ _ _ _} _.
|
