Demo of the ShotTo NCPO Implementation

Copy Markdown View Source
Run in Livebook 
Mix.install([
  {:shot_to, path: Path.join(__DIR__, "..")}
])

Setup

import ShotDs.Hol.Sigils
import ShotDs.Hol.Definitions

NCPO Test Cases

with_context(~e[], fn ->
  ShotTo.compare(
    equals_term(type_i()),
    ~f"^[X:$i, Y:$i]: ![P:$i>$o]: P @ X => P @ Y"
  )
end)