• Raphael Rieu-Helft's avatar
    Add support for partial functions · 17ed1270
    Raphael Rieu-Helft authored
    Program functions can be declared as partial with "let/val partial".
    Similarly to "diverges", partial code cannot be ghost, however it does not need to be
    explicitly specified as partial.
    
    Fixes #184.
    17ed1270
Name
Last commit
Last update
..
7.why Loading commit data...
bad_type_arity1.why Loading commit data...
bad_type_arity2.why Loading commit data...
cast1.why Loading commit data...
clash1.why Loading commit data...
clash_axiom1.why Loading commit data...
clash_builtin1.why Loading commit data...
clash_logic1.why Loading commit data...
clash_type1.why Loading commit data...
clash_type2.why Loading commit data...
clash_type3.why Loading commit data...
clash_type4.why Loading commit data...
clausal1.why Loading commit data...
clausal2.why Loading commit data...
clausal3.why Loading commit data...
clone_record1.mlw Loading commit data...
clone_record2.mlw Loading commit data...
coercion_already.mlw Loading commit data...
coercion_already1.mlw Loading commit data...
coercion_already3.mlw Loading commit data...
coercion_cycle1.mlw Loading commit data...
coercion_cycle2.mlw Loading commit data...
coercion_cycle3.mlw Loading commit data...
coercion_type_args1.mlw Loading commit data...
coercion_type_args2.mlw Loading commit data...
coercion_type_args3.mlw Loading commit data...
coercion_type_args4.mlw Loading commit data...
coercion_type_args5.mlw Loading commit data...
cyclic_type1.why Loading commit data...
cyclic_type2.why Loading commit data...
duplicate_type_parameter1.why Loading commit data...
linearity1.why Loading commit data...
partial_function.mlw Loading commit data...
partial_ghost.mlw Loading commit data...
partial_ghost_fun.ml Loading commit data...
partial_ghost_fun.mlw Loading commit data...
partial_ghostvar.mlw Loading commit data...
partial_lemma.mlw Loading commit data...
partial_terminates.mlw Loading commit data...
partial_witness.mlw Loading commit data...
pat_linearity1.why Loading commit data...
pat_linearity2.why Loading commit data...
pat_linearity3.why Loading commit data...
record2.why Loading commit data...
record3.why Loading commit data...
record4.why Loading commit data...
record5.why Loading commit data...
record6.why Loading commit data...
record7.why Loading commit data...
record8.why Loading commit data...
record9.why Loading commit data...
stdlib_c1.mlw Loading commit data...
stdlib_c2.mlw Loading commit data...
stdlib_c3.mlw Loading commit data...
stdlib_c4.mlw Loading commit data...
stdlib_c5.mlw Loading commit data...
stdlib_c6.mlw Loading commit data...
unbound_namespace1.why Loading commit data...
unbound_theory1.why Loading commit data...
unbound_type1.why Loading commit data...
unbound_type_var1.why Loading commit data...
undefined_type_var1.why Loading commit data...
undefined_type_var2.why Loading commit data...
wf_types1.why Loading commit data...
wf_types2.why Loading commit data...
wf_types3.why Loading commit data...