Stream: Coq users

Topic: Is `Bind Scope` ignored by `let`?


view this post on Zulip Paolo Giarrusso (Dec 02 2020 at 15:51):

I'm not sure why : ptr doesn't avoid needing %ptr below.

(* SETUP *)
  Definition ptr : Set := ....
  Declare Scope ptr_scope.
  Bind Scope ptr_scope with ptr.
  Delimit Scope ptr_scope with ptr.
  Notation "p .., o" := (_offset_ptr p o) : ptr_scope.

(* TEST *)
  Definition foo p o : ptr := p .., o.
  Fail Definition foo' p o : ptr :=
    let p' : ptr := (p .., o) in
    p'.
  Definition foo' p o : ptr :=
    let p' : ptr := (p .., o)%ptr in
    p'.

Last updated: Feb 06 2023 at 13:03 UTC