Stream: Coq users

Topic: `if` vs `match` in printing, `case_style`


view this post on Zulip Paolo Giarrusso (Oct 07 2022 at 17:48):

if can mean match internally, so how does the pretty-printer tell them apart?

Inductive Op : Set := | Read | Write.

Definition write_op (evt : Op) : bool :=
  match evt with
  | Write => true
  | Read => false
  end.
Definition write_op' (evt : Op) : bool :=
  if evt then false else true.
Print write_op.
Print write_op'.

Is the parser just storing the appropriate case_style value (type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle), just to preserve this in printing?


Last updated: Sep 28 2023 at 11:01 UTC