application of higher-order record field's terms to arguments
There is a missing feature in Necro. Here's an example:
term intOne : int
term intSucc : int -> int
type intRec = ( __Succ__ : int -> int)
term test : intRec = (__Succ__ = intSucc)
term succTest : (ir : intRec) -> int =
ir.__Succ__ intOne
It works only if we explicitly define an application term
term intOne : int
term intSucc : int -> int
type intRec = ( __Succ__ : int -> int)
term test : intRec = (__Succ__ = intSucc)
term succTest : (ir : intRec) -> int =
app<int,int> ir.__Succ__ intOne
term app<a,b> : (f : a -> b) -> (args : a) -> b =
f args
But this is just a work-around, and indeed implies to carry on all the type informations, which can grow arbitrarily large
Edited by KHAYAM Adam