fact: Definition specific_meaning_apply2 {A B : SimpleTypeCode} {C} {C'} (syntactify : C' -> normalized_of (range_of C)) (f : onelevelG A -> onelevelG B -> C') (args : arg_meanings_for (A --> B --> C)) : option (normalized_of (range_of (A --> B --> C))) := match constantOf (ahd args), constantOf (ahd (atl args)) with | Some v0, Some v1 => Some (syntactify (f v0 v1)) | _, _ => None end.
imports: Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics Fiat.Parsers.Reflective.Syntactify Fiat.Common Fiat.Common.NatFacts Fiat.Common.List.Operations