[Agda] Strict application

[Andrés Sicard-Ramírez]

On 26 April 2014 10:28, Wolfram Kahl <kahl at cas.mcmaster.ca> wrote:

> > {-# NO_TERMINATION_CHECK #-}
> > loop : ℕ
> > loop = loop
> >
> > foo : ℕ
> > foo = (λ _ → 0) loop
>
> This is not Agda code (or, if you want, is is ``illegal Agda code''):
> You are only allowed to use {-# NO_TERMINATION_CHECK #-}
> where you have a separate termination proof.
>

I agree. That is ``illegal Agda code''.

Let _≡_ be the propositional equality. I can formalise a non-strict
application (beta) by

postulate
  D    : Set
  app  : D → D → D
  lam  : (D → D) → D
  beta : ∀ f a → app (lam f) a ≡ f a

Using the same approach, can I formalise a strict application?

Best,

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140426/c02a5618/attachment.html