fact: Definition pb_check_level (hiding : bool) (ch : Char) (start_level : nat) : bool := if is_bin_op ch then if hiding then Compare_dec.gt_dec start_level 0 : bool else true else if is_open ch then true else if is_close ch then (Compare_dec.gt_dec start_level 0 : bool) else true.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Common.List.Operations Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.Enumerable Fiat.Common.LogicFacts Fiat.Common.Equality