Consider:
#include "share/atspre_staload.hats"
fun only_zero(n: int(0)): void =
println!("This is definitely zero: ", n)
fun less_than{n,m:int | n < m}(n: int(n), m: int(m)): void =
println!(n, " is less than ", m)
implement main0() = (
only_zero(zeroify(n));
only_zero(m);
less_than(b, a);
less_than(f, e) where { val (f, e) = make_less_than((d, c)) };
) where {
val n = 5
val m = ~5
val (a, b, c, d) = (1, 2, 3, 4)
extern castfn zeroify{n:int}(n: int(n)): int(0)
extern praxi lemma_this_is_zero{n:int}(n: int(n)): [n == 0] void
extern castfn make_less_than{n,m:int}(t: (int(n), int(m))): [o,p:int | o < p] (int(o), int(p))
extern praxi lemma_less_than{n,m:int}(n: int(n), m: int(m)): [n < m] void
prval _ = lemma_this_is_zero(m)
}
which has this output:
This is definitely zero: 5
This is definitely zero: -5
2 is less than 1
4 is less than 3
Are there cases that demand one of these over the other?
If you use 'castfn', you need to make sure that there is a corresponding implicit cast function in the target language. For instance, int2double is a castfn if C is the target language.
On the other hand, praxi/prfun is completely erased, having no trace in the generated code.
I would say that praxi/prfun is more general, but int2double is definitely not a praxi/prfun.