fact: Definition possible_open_closes : list (Ascii.ascii * Ascii.ascii) := Operations.List.uniquize Equality.beq (List.flat_map (fun openf_closef => let openf := fst openf_closef in let closef := snd openf_closef in let opens := List.filter openf (Enumerable.enumerate Ascii.ascii) in let closes := List.filter closef (Enumerable.enumerate Ascii.ascii) in match opens, closes with | cho::nil, chc::nil => if ascii_beq cho chc then nil else [(cho, chc)] | _, _ => nil end) possible_open_closes_pre).
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Computation.Refinements.General Fiat.Common Fiat.Common.Equality Fiat.Common.List.Operations Fiat.Computation.Refinements.General Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.Reachable.ParenBalancedHiding.Core Fiat.Parsers.Refinement.DisjointRulesCommon Fiat.Parsers.Refinement.BinOpBrackets.ParenBalanced Fiat.Parsers.Refinement.BinOpBrackets.MakeBinOpTable Fiat.Parsers.Refinement.BinOpBrackets.ParenBalancedLemmas Fiat.Parsers.Refinement.BinOpBrackets.ParenBalancedGrammar Fiat.Parsers.Refinement.PossibleTerminalsSets Fiat.Parsers.ParserInterface Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Valid Fiat.Parsers.ContextFreeGrammar.ValidProperties Fiat.Parsers.ContextFreeGrammar.ValidReflective Fiat.Parsers.Splitters.RDPList Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.Refinement.PreTactics Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.Refinement.DisjointLemmas