idris-lang/Idris-dev — pull request #1484 by edwinb (2014-08-21 21:41:22+00:00)
Title: Add Borrowed types

This allows unique values to be inspected, but not updated or
destroyed. A 'Borrowed' value can be pattern matched, but cannot be used
on the right hand side, nor can any Unique values contained in the
pattern.