Foldl.hascasl.output revision 4d5d65e4f55ba8eaa02a4dab14348abeda75cf6b
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancetype List(a : Type)
81ec673ac5ab1493568d9ef7798b752ab8ee0e61Felix Gabriel Manceop nil : List a
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceop head : List a -> a
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceop snoc : List a -> a --> List a
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance. ((fun __=__[List a] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
5d801400993c9671010d244646936d8fd435638cChristian Maeder List a * List a ->? Unit)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ((((op snoc[a]
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance : forall a : Type . List a_v-1 -> a_v-1 --> List a_v-1) :
aa0ca44e856c87db27e61687cbb630f270976da1Felix Gabriel Mance List a -> a --> List a)
5d801400993c9671010d244646936d8fd435638cChristian Maeder ((op nil[a] : forall a : Type . List a_v-1) : List a) :
5d801400993c9671010d244646936d8fd435638cChristian Maeder a --> List a)
5d801400993c9671010d244646936d8fd435638cChristian Maeder (var x : a) :
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mance : forall a : Type . List a_v-1 -> a_v-1 --> List a_v-1) :
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance List a -> a --> List a)
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder ((op nil[a] : forall a : Type . List a_v-1) : List a) :
090c663fcc1593c66f39a0972326799a672760d5Christian Maeder a --> List a)
f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian Maeder (var x : a) :
18ff56829e5e99383ee6106584d55bcbd8ed45e7Felix Gabriel Mance. ((fun __=__[a] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance a * a ->? Unit)
b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder ((((op head[a ->? a] : forall a : Type . List a_v-1 -> a_v-1) :
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance List (a ->? a) -> a ->? a)
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance ((op nil[a ->? a] : forall a : Type . List a_v-1) :
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance List (a ->? a)) :
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance%% Type Constructors -----------------------------------------------------
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceList : Type -> Type
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceLogical : Type := Unit ->? Unit
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancePred : Type -> Type := \ a : Type . a_v-1 ->? Unit
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance__*__ : +Type -> +Type -> Type
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance__-->?__ : -Type -> +Type -> Type < __->?__
0ec1551231bc5dfdcb3f2bd68fec7457fade7bfdFelix Gabriel Mance__->__ : -Type -> +Type -> Type < __->?__
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance__->?__ : -Type -> +Type -> Type
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maedera : Type %(var_1)%
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder%% Assumptions -----------------------------------------------------------
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance__/\__ : ? Unit * ? Unit ->? Unit %(fun)%
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance__=>__ : ? Unit * ? Unit ->? Unit %(fun)%
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance__\/__ : ? Unit * ? Unit ->? Unit %(fun)%
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance__if__ : ? Unit * ? Unit ->? Unit %(fun)%
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance : forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%
68de80eb2800338cbd16512106fcadab79325d8bChristian Maederbottom : forall a : Type . a_v-1 %(fun)%
68de80eb2800338cbd16512106fcadab79325d8bChristian Maederdef__ : forall a : Type . a_v-1 ->? Unit %(fun)%
68de80eb2800338cbd16512106fcadab79325d8bChristian Maederfalse : Unit %(fun)%
68de80eb2800338cbd16512106fcadab79325d8bChristian Maederhead : forall a : Type . List a_v-1 -> a_v-1 %(op)%
68de80eb2800338cbd16512106fcadab79325d8bChristian Maedernil : forall a : Type . List a_v-1 %(op)%
68de80eb2800338cbd16512106fcadab79325d8bChristian Maedernot__ : ? Unit ->? Unit %(fun)%
68de80eb2800338cbd16512106fcadab79325d8bChristian Maedersnoc : forall a : Type . List a_v-1 -> a_v-1 --> List a_v-1 %(op)%
fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian Maedertrue : Unit %(fun)%
fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian Maeder�__ : ? Unit ->? Unit %(fun)%
68de80eb2800338cbd16512106fcadab79325d8bChristian Maeder%% Sentences -------------------------------------------------------------
fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian Maeder((fun __=__[List a] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance List a * List a ->? Unit)
68de80eb2800338cbd16512106fcadab79325d8bChristian Maeder ((((op snoc[a]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance : forall a : Type . List a_v-1 -> a_v-1 --> List a_v-1) :
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance List a -> a --> List a)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ((op nil[a] : forall a : Type . List a_v-1) : List a) :
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder a --> List a)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance : forall a : Type . List a_v-1 -> a_v-1 --> List a_v-1) :
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance List a -> a --> List a)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ((op nil[a] : forall a : Type . List a_v-1) : List a) :
544989bc1f6ed4bc0813334ffd934db0fb0010eaFelix Gabriel Mance((fun __=__[a] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
544989bc1f6ed4bc0813334ffd934db0fb0010eaFelix Gabriel Mance a * a ->? Unit)
544989bc1f6ed4bc0813334ffd934db0fb0010eaFelix Gabriel Mance ((((op head[a ->? a] : forall a : Type . List a_v-1 -> a_v-1) :
544989bc1f6ed4bc0813334ffd934db0fb0010eaFelix Gabriel Mance List (a ->? a) -> a ->? a)
f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian Maeder ((op nil[a ->? a] : forall a : Type . List a_v-1) :
f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian Maeder List (a ->? a)) :
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance%% Diagnostics -----------------------------------------------------------
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance*** Hint 1.5, is type variable 'a'
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder*** Hint 6.9, not a class 'a'