[Agda] Termination not being proven

[Nils Anders Danielsson]

On 2011-03-02 14:16, Will Sonnex wrote:
> Is there a way in Agda to define an arbitrary subset of Set, say
> "Hask" for Haskell types. One could use this to accept potentially
> non-terminating values and then even if one could define "inhabited :
> {A : Hask} →A", it could only ever be applied to other Hask types. As
> long as we did not take inhabitance of a Hask type to be a sound proof
> I think (tentatively) that the overall system would be sound.

You cannot define "subsets" of this kind, but you can define something
similar:

   mutual

     data Hask : Set where
       ⋮

     El : Hask → Set
     ⋮

In this case it seems as if you would want to encode some notion of
pointed CPOs, which are always inhabited:

   ⊥ : {A : Hask} → El A

-- 
/NAD