fact: Definition paren_balanced'_step (ch : Char) (pbh_rest : nat -> bool) (start_level : nat) : bool := if is_bin_op ch then pbh_rest start_level else if is_open ch then pbh_rest (S start_level) else if is_close ch then ((Compare_dec.gt_dec start_level 0) && pbh_rest (pred start_level))%bool else pbh_rest start_level.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Common