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).
Please advice, where is my mistake?