Interleaving type checking and termination checking

[agda]

Interleaving type checking and termination checking

[GoogleCodeExporter]

Original comment by [email protected] on 23 Jan 2008 at 9:54

• Changed state: Accepted
• Added labels: Priority-Low
• Removed labels: Priority-Medium

[GoogleCodeExporter]

Original comment by [email protected] on 11 Jun 2008 at 12:59

• Changed title: Interleaving type checking and termination checking
• Added labels: Type-Enhancement
• Removed labels: Type-Defect

[GoogleCodeExporter]

> The emacs mode gets confused when agda does not respond. Ctrl-g
> gives back the cursor, but the process is still tied up in the
> background.

Nowadays you can restart the process by invoking agda2-restart
(C-c C-x C-r).

Original comment by nils.anders.danielsson on 1 Feb 2009 at 4:05

[GoogleCodeExporter]

Issue 201 has been merged into this issue.

Original comment by nils.anders.danielsson on 25 Sep 2009 at 2:45

[GoogleCodeExporter]

Issue 371 has been merged into this issue.

Original comment by nils.anders.danielsson on 30 Dec 2010 at 11:37

[GoogleCodeExporter]

Issue 379 has been merged into this issue.

Original comment by [email protected] on 21 Jan 2011 at 1:52

[GoogleCodeExporter]

Issue 385 has been merged into this issue.

Original comment by nils.anders.danielsson on 11 Feb 2011 at 11:41

[GoogleCodeExporter]

Issue 653 has been merged into this issue.

Original comment by [email protected] on 21 May 2012 at 12:47

[GoogleCodeExporter]

Issue 801 has been merged into this issue.

Original comment by nils.anders.danielsson on 27 Feb 2013 at 9:45

[GoogleCodeExporter]

This was fixed by Andreas in February.

Original comment by [email protected] on 9 Nov 2013 at 2:56

• Changed state: Fixed

[GoogleCodeExporter]

Andreas has recently added another mechanism that can be used to
trigger non-termination:

  p : Σ ℕ λ n → n ≡ 0
  proj₁ p = proj₁ p
  proj₂ p = refl

Mutual blocks can also be used:

  mutual

    Foo : Set
    Foo = Foo

    foo : Foo
    foo = foo

Original comment by nils.anders.danielsson on 11 Nov 2013 at 1:59

• Changed state: Accepted