# Tvals in my code is the total map, why coq insists it is not?

Hello, I am not able to make this code work.
I expect that tvals in formulaTrue inductive type is a total map. So I should be able to check in
TVar constructor if (tvals var) equals true or not. But Coq gives an error:

Error: Illegal application (Non-functional construction):
The expression “tvals” of type “Type” cannot be applied to the term
“var” : “?T”

``````Definition var := nat % type.

Definition total_map (A : Type) := var -> A.

Definition t_empty {A : Type} (v : A) : total_map A :=
(fun _ => v).

Definition t_update {A : Type} (m : total_map A)
(x : var) (v : A) :=
fun x' => if PeanoNat.Nat.eqb x x' then v else m x'.

Definition tvals := total_map bool.

Inductive formula : Set :=
| Var : var -> formula.

Inductive formulaTrue : tvals -> formula -> Prop :=
| TVar : forall var, tvals var = true -> formulaTrue tvals (Var var).
``````

The identifier `tvals` in the definition of `TVar` should refer to an inhabitant of the type `tvals` that you define beforehand, so you should quantify over this identifier at the same time as `var` (and maybe rename it to `tv` to lessen the confusion):

``````Inductive formulaTrue : tvals -> formula -> Prop :=
| TVar : forall tv var, tv var = true -> formulaTrue tv (Var var).
``````
1 Like

Hello,

You have defined `tvals` as the type of functions from `var` to `bool`. You can therefore apply any element in this type to a variable, but not the type itself. Currently, it is as if you were trying to use `var` as a specific natural number.

You probably meant to write:

``````Inductive formulaTrue : tvals -> formula -> Prop :=
| TVar : forall map var, map var = true -> formulaTrue map (Var var).
``````

EDIT: Woops, too slow

1 Like

Thank you, I got it.