git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/docs002/docs002.idr
17 lines 382 B history raw
1module Main
3-- Simple test case for type provider documentation.
4%language TypeProviders
6getType : Int -> IO (Provider Type)
7getType 0 = pure (Provide Int)
8getType _ = pure (Provide Bool)
10||| Some documentation
11%provide (T1 : Type) with getType 0
13||| Some other documentation
14%provide (T2 : Type) with getType 1
16||| Some provided postulate
17%provide postulate T3 with getType 0