Opened 2 years ago

Last modified 17 months ago

#411 new feature

Allow types of pattern binders to be specified in source language

Reported by: benl Owned by:
Priority: normal Milestone:
Component: Source Parser Version: 0.4.2
Keywords: Cc:

Description

The following works in Core Tetra but not in Source Tetra.

data Foo where
        Foo : Nat# -> Foo

foo (x: Foo): Bool#
 = case x of
        Foo (x: Nat#) -> True

Make it accept the (x: Nat#) annotation.

Change History (2)

comment:1 Changed 17 months ago by benl

  • Summary changed from Allow types of pattern binders to be specified in Source Tetra to Allow types of pattern binders to be specified in source language
  • Type changed from enhancement to feature

comment:2 Changed 17 months ago by benl

  • Component changed from Unknown to Source Parser
Note: See TracTickets for help on using tickets.