fn parse_reft_func(cx: &mut ParseCtxt<'_>) -> ParseResult<SpecFunc>
Expand description
⟨func_def⟩ := ⟨ # [ hide ] ⟩?
fn ⟨ident⟩ ⟨ < ⟨ident⟩,* > ⟩?
( ⟨refine_param⟩,* )
->
⟨sort⟩
fn parse_reft_func(cx: &mut ParseCtxt<'_>) -> ParseResult<SpecFunc>
⟨func_def⟩ := ⟨ # [ hide ] ⟩?
fn ⟨ident⟩ ⟨ < ⟨ident⟩,* > ⟩?
( ⟨refine_param⟩,* )
->
⟨sort⟩