`|>` と `|>.` は別の構文である

lean-ja / lean-by-example

コード例で学ぶ Lean 言語

https://lean-ja.github.io/lean-by-example/

MIT License

51 stars 7 forks source link

`|>` と `|>.` は別の構文である #1124

Open Seasawher opened 1 week ago

Seasawher commented 1 week ago

パイプラインって意外と難しいね

Zulip: > Style question: space between '|>' and '.'?

opaque A : Type
opaque B : Type

axiom a : A
axiom A.f : A → B
axiom B.f : A → B

set_option pp.fieldNotation.generalized false

/-- info: B.f a : B -/
#guard_msgs in
#check (a |> .f : B)

/-- info: A.f a : B -/
#guard_msgs in
#check (a |>.f : B)