call and type arguments

[weaversa]

Say I have the following function:

f : {n} (fin n) => Bit
f = `n > 0

How do I use the call interface to do the following:

Main> f `{100}
True
Main> f `{0}
False

Does the expression string accept something like f`{10}?

[david-christiansen]

The expression may be any JSON representation of a Cryptol expression, including strings with concrete syntax in them, and that concrete syntax may be an arbitrary expression. Example:

2020-04-20 09:31:51	sent	{"jsonrpc":"2.0","id":2,"method":"evaluate expression","params":{"state":[["load file",{"file":"/home/dtc/Projects/proto/proto/Foo.cry"}]],"expression":"all `{n=0}"}}
2020-04-20 09:31:51	reply	{"error":{"data":{"type string":"{a} (a -> Bit) -> [0]a -> Bit","type":{"propositions":[],"forall":[{"kind":"Type","name":"a"}],"type":{"domain":{"domain":{"kind":"Type","name":"a","type":"variable"},"range":{"type":"Bit"},"type":"function"},"range":{"domain":{"length":{"value":0,"type":"number"},"contents":{"kind":"Type","name":"a","type":"variable"},"type":"sequence"},"range":{"type":"Bit"},"type":"function"},"type":"function"}}},"code":20200,"message":"Can't evaluate at polymorphic type"},"jsonrpc":"2.0","id":2}

We probably should add a higher-level syntax for specifying type arguments, however. String interpolation is not great, especially if you want to instantiate them with other types that have been received in a structured format.

[weaversa]

I asked how to use the call method to specify type arguments. Your example uses the expression method. Is it not possible using call?