fact: Fixpoint interp_RCharExpr (expr : RCharExpr Char) : Char -> bool := match expr with | rbeq ch => irbeq ch | ror a b => fun ch => interp_RCharExpr a ch || interp_RCharExpr b ch | rand a b => fun ch => interp_RCharExpr a ch && interp_RCharExpr b ch | rneg x => fun ch => negb (interp_RCharExpr x ch) | rcode_le_than code => fun ch => BinNat.N.leb (irN_of ch) code | rcode_ge_than code => fun ch => BinNat.N.leb code (irN_of ch) end%bool.
imports: Coq.Strings.Ascii Fiat.Parsers.ContextFreeGrammar.Core Fiat.Common.Equality