git.iko.soy/Idris-dev
on 7d42ba2 help sign in
Idris-dev/test/docs002/docs002.idr
20 lines 405 B history raw
1module Main
3-- Simple test case for type provider documentation.
5import Providers
7%language TypeProviders
9getType : Int -> IO (Provider Type)
10getType 0 = return (Provide Int)
11getType _ = return (Provide Bool)
13||| Some documentation
14%provide (T1 : Type) with getType 0
16||| Some other documentation
17%provide (T2 : Type) with getType 1
19||| Some provided postulate
20%provide postulate T3 with getType 0