search

JetBrains / intellij-arend

Arend plugin for IntelliJ IDEA
Apache License 2.0
90 stars 12 forks source link

Completion does not work after a dot in meta expressions #461

Open valis opened 8 months ago

valis commented 8 months ago

For example, field is not completed in the following code:

\record R (field : Nat)

\func axsax => ∃ (r : R) (r.field = 0)