Module Qcert.Imp.Lang.ImpDataSize

Require Import String.
Require Import Lia.
Require Import EquivDec.
Require Import Decidable.
Require Import Utils.
Require Import DataRuntime.
Require Import Imp.
Require Import ImpData.
Require Import ImpSize.

Section ImpDataSize.

  Context {fruntime:foreign_runtime}.

  Definition imp_data_expr_size (e:imp_data_expr) : nat :=
    imp_expr_size e.

  Definition imp_data_stmt_size (stmt:imp_data_stmt) : nat :=
    imp_stmt_size stmt.

  Definition imp_data_function_size (q:imp_data_function) : nat :=
    imp_function_size q.

  Definition imp_data_size (q: imp_data) : nat :=
    imp_size q.

End ImpDataSize.