Skip to content

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

Open
@valis

Description

@valis

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

\record R (field : Nat)

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

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions