fact: Definition run (m : nat) (e : Expr) := match makeTriplets (norm e) with | tRC L r n => letP _ _ (buildL L) (fun Ar => letP _ _ (nat_of_P (valRz r)) (fun n => stal (getT Ar) n m (rArrayInit _ (fun r => class nil)) r rZFalse)) end.
imports: Coq(ZArith)