on 8fe28aa help sign in
12 lines 276 B history raw
1T1 : Type
2 Some documentation
3
4 The function is: Total & public export
5T2 : Type
6 Some other documentation
7
8 The function is: Total & public export
9T3 : Int
10 Some provided postulate
12 The function is: not yet checked for totality & public export