packages feed

idris-0.9.17.1: test/reg061/Capture.idr

module Capture

-- Test for variable capture in syntax

syntax delay  [x] = \z => case z of { () => x }
syntax delay' [z] = delay z

capture : a -> () -> a
capture x = delay' x