idris-0.9.9: test/test023/test023.idr

module Main

-- Simple test case for trivial type providers.

import Providers

%language TypeProviders

-- Provide the Unit type
goodProvider : IO (Provider Type)
goodProvider = return (Provide (the Type ()))

%provide (Unit : Type) with goodProvider

foo : Unit
foo = ()

-- Always fail
badProvider : IO (Provider Type)
badProvider = return (Error "Always fails")

%provide (t : Type) with badProvider