Agda is a dependently typed programming language / interactive theorem prover.
Home Page: https://wiki.portal.chalmers.se/agda/pmwiki.php
License: Other
Note that this README is only about Agda, not its standard library. See the Agda Wiki for information about the library.
HACKING
For example
postulate test :
Set
generates a parse error
Original issue reported on code.google.com by [email protected] on 4 Nov 2007 at 7:44
If I refine (C-c C-r) in
fun : ...
fun = {\x -> ?}
I got
fun = \x' -> { }
instead of
fun = \x -> { }.
The same happens if I use 'y' instead of 'x', but it does not happen if I
use others variables names (e.g. 'a', 'b', 'xxx', etc).
Original issue reported on code.google.com by [email protected] on 27 Jan 2008 at 4:34
running
agda -v10 Bad2.agda
loops. As far as our analysis is concerned, pretty printing of the term
bad2 x + bad2 (succ x)
hangs agda.
Pretty printing of terms is invoked in
Termination/TermCheck.hs
termTerm :: MutualNames → QName → [DeBruijnPat] → Term → TCM Calls
termTerm names f pats0 t0 = do
reportSDoc “term.check.clause” 10
(sep [ text “termination checking clause of” <+> prettyTCM f
, nest 2 $ text “lhs:” <+> hsep (map prettyTCM pats0)
, nest 2 $ text “rhs:” <+> prettyTCM t0
])
in
prettyTCM t0
Original issue reported on code.google.com by [email protected] on 24 Oct 2007 at 10:54
A.agda:
module A where
data B : Set where
Bug.agda:
module Bug where
open import A public using () renaming (B to C)
open import A
Foo : Set
Foo = C
Error message:
Bug.agda:7,7-8
Ambiguous name C. It could refer to any one of
.Bug._.B bound at A.agda:3,6-7
B bound at A.agda:3,6-7
when scope checking C
C has only been brought into scope once, so this is strange.
Maybe one should not import a module twice, but in that case an error
should be reported when the second import statement is checked.
Original issue reported on code.google.com by nils.anders.danielsson on 11 Dec 2007 at 2:38
The use of a@ in this code fragment
accSucc : (x : Nat) → Acc Nat Lt x → Acc Nat Lt (succ x)
accSucc x a@(acc .x h) = acc (succ x) (\ y p → ltcase y x p (Acc Nat Lt) h a)
causes a Panic:
BUG-THINGOUTOFCXT.agda:26,77–78
Panic: thing out of context ([CtxId 147,CtxId 146] not prefix of
[CtxId 149,CtxId 148,CtxId 147,CtxId 146])
when checking that the expression a has type Acc Nat Lt x
Original issue reported on code.google.com by [email protected] on 24 Oct 2007 at 10:50
Attachments:
module Bug where
record AR : Set1 where
field
a : Set
x : a
module M (A : AR) where
record MR : Set1 where
field F : AR.a A -> Set
record BR (A : AR) (AF : M.MR A) : Set where
open AR A
open M A
field f : forall {B} -> MR.F x
*** Exception: src/full/TypeChecking/Substitute.hs:115: the impossible happened
Original issue reported on code.google.com by nils.anders.danielsson on 11 Dec 2007 at 4:02
module Bug where
data _≡_ {a : Set} (x : a) : a -> Set where
≡-refl : x ≡ x
record _×_ (a b : Set) : Set where
field
proj₁ : a
proj₂ : b
open _×_
foo : forall {a b} (x : a × b) ->
record {proj₁ = proj₁ x; proj₂ = proj₂ x} ≡ x
foo x with proj₁ x | proj₂ x
foo x | x₁ | x₂ = ?
-- ?0 : record {proj₁ = x₁; proj₂ = x₂} ≡ x
Original issue reported on code.google.com by nils.anders.danielsson on 11 Dec 2007 at 12:24
*** Exception: fromUTF8: Bad utf-8 character: '\161'
I don't know how I got the ¡ instead of the |!
But then ctrl c-x-l gets silly
What version of the product are you using? On what operating system?
Agda 2 version 2.1.3
on linux
Original issue reported on code.google.com by [email protected] on 6 Nov 2007 at 1:34
What the summary says.
Original issue reported on code.google.com by [email protected] on 24 Oct 2007 at 10:34
If you type this:
record X : Set where
field Y : ?
You get the error:
Field appearing outside record declaration.
when checking the definition of X
Original issue reported on code.google.com by [email protected] on 4 Dec 2007 at 1:56
Is this intended?
module Bug where
record A : Set1 where
field foo : Set
record B (x : A) : Set1 where
open A x
field foo : Set
Bug.agda:8,9-18
Multiple definitions of foo. Previous definition at
Bug.agda:4,9-12
when scope checking the declaration
field foo : Set
Original issue reported on code.google.com by nils.anders.danielsson on 11 Dec 2007 at 7:19
I am quite fond of shadowing when writing programs. I think it is a good safety feature. Often you might do an intermediate computation which makes an earlier argument x meaningless and it is a good thing that you can no longer refer to it, having to a more local similar thing a name like x' just increases the change of a silly mistake. This practice is currently disallowed by with. Here's a silly example:
g : Set -> Set
g = ?
f : Set -> Set
f p with g p
... | p = ?this gives the error:
Repeated variables in left hand side: p
when scope checking the left-hand side f p in the definition of fI think that the original p should get replaced by _ in the helper function if its name has been captured.
Original issue reported on code.google.com by [email protected] on 29 Nov 2007 at 10:51
Problem:
In emacs, I want to use the --no-coverage-check flag, so I write
{-# OPTIONS --no-coverage-check #-}
Now, I do not want to use it, so I erase the previous line, but Agda
continues working in "no coverage check" mode.
What version of the product are you using? Darcs version pulled after
2008-01-16
On what operating system? Ubuntu, 7.10
Original issue reported on code.google.com by [email protected] on 26 Jan 2008 at 1:18
module Bug where
data K : Set where
a : K
b : K
data T : K -> Set where
ta : T a
tb : T b
f : forall k -> T k
f a = ta
f b = tb
data D : forall {k} (t : T k) -> Set where
c : forall {k} -> D (f k)
-- This function does not type check. It would type check if the
-- constraint k = a were solved before the constraint f k = f a.
foo : forall {t : T a} -> D t -> D t -> Set
foo c (c {k = a}) = K
Original issue reported on code.google.com by nils.anders.danielsson on 19 Oct 2007 at 3:10
module Bug where
record Foo (F : Set -> Set) : Set1 where
record Bar (F : Set -> Set) : Set1 where
field foo : Foo F
open Foo foo public
field bar : Set
Error message:
Let-definitions cannot do pattern matching or be recursive.
when scope checking
let open module _ = Foo foo public in (bar : Set) -> Prop
The let definition above does not use pattern matching, nor is it recursive.
Original issue reported on code.google.com by nils.anders.danielsson on 11 Dec 2007 at 7:38
The literate agda files yield a lexical error (after to compile with ghc 6.8.1)
Version: Darcs repository on 20071117
Original issue reported on code.google.com by [email protected] on 17 Nov 2007 at 1:56
It should be possible to detect termination when an argument is smaller
than a dotted pattern. For instance, the following code should terminate:
module Test where
data Nat : Set where
zero : Nat
suc : Nat → Nat
data Bool : Set where
true : Bool
false : Bool
_&&_ : Bool → Bool → Bool
true && b = b
false && b = false
data Ty : {_ : Nat} → Set where
Base : forall {n} → Ty {suc n}
Arr : forall {n} → Ty {n} → Ty {n} → Ty {suc n}
subty : forall {n} → Ty {n} → Ty {n} → Bool
subty Base Base = true
subty (Arr σ τ) (Arr σ’ τ’) = subty σ’ σ && subty τ τ’
subty _ _ = false
Currently the termination checker cannot see that in both the two recursive
calls of subty the first (hidden) argument is strictly smaller than on the LHS.
Andreas: Discussed that with Ulf. The internal syntax erases the dotted
patterns constructed during pattern checking. This is an optimization for
speeding up execution, but the “logical” reading (fully reconstruced form)
of the second clause is
subty {suc n} (Arr {n} σ τ) (Arr {n} σ’ τ’) = subty {n} σ’ σ && subty {n} τ τ’
To keep internally a fully reconstructed form is probably not only useful
for the termination checker but also for other static analyses.
To print back the fully reconstructed form, as for instance Twelf does, is
also a good feedback to the user: He sees how the system “understood” his
input, and he can check that it understood it correctly. See
Main.PrintReconstructedTerms feature request.
Original issue reported on code.google.com by [email protected] on 24 Oct 2007 at 10:44
You should be able to do this:
module Test where
data Nat : Set where
zero : Nat
suc : Nat -> Nat
data Vec : Nat -> Set where
[] : Vec zero
_::_ : {n : Nat} -> Nat -> Vec n -> Vec (suc n)
f : (n : Nat) -> Vec n -> Nat
f n@._ [] = n
Original issue reported on code.google.com by [email protected] on 24 Oct 2007 at 10:32
Recently there was no highlighting for operators with termination problems,
and now there is no highlighting for operators with unsolved meta
variables. Example:
module Bug where
foo_ : {a : Set} → Set1 → Set1
foo_ x = x
bar : Set1
bar = foo Set
The last occurrence of foo should be highlighted, but it is not.
The reason for these problems is that operator ranges are represented in a
stupid way. We can fix the particular problem above with another hack, but
I would prefer if the root of these problems could be fixed.
Original issue reported on code.google.com by [email protected] on 24 Oct 2007 at 10:37
Compilation stops with the following error:
error: ../../undefined.h: No such file or directory
The complete build log:
$ runhaskell Setup.hs configure --user --prefix=/home/user/cabal
Configuring Agda-2.1.2...
Warning: No license-file field.
checking for gcc... gcc
checking for C compiler default output file name... a.out
checking whether the C compiler works... yes
checking whether we are cross compiling... no
checking for suffix of executables...
checking for suffix of object files... o
checking whether we are using the GNU C compiler... yes
checking whether gcc accepts -g... yes
checking for gcc option to accept ISO C89... none needed
checking for ghc... ghc
checking for ghc version... 6.6.1
checking for alex... alex
checking for alex version... 2.1.0
checking for happy... happy
checking for happy version... 1.16
checking for haddock... haddock
checking for haddock version... 0.8
checking for latex... latex
checking for pdflatex... pdflatex
checking for a BSD-compatible install... /usr/bin/install -c
checking for wget... wget
checking for false... false
checking for find... find
checking for diff... diff
checking for darcs... darcs
checking for mkdir... mkdir
checking for hasktags... hasktags
checking for runhaskell... runhaskell
configure: creating ./config.status
config.status: creating mk/config.mk
$ runhaskell Setup.hs build
Preprocessing library Agda-2.1.2...
Building Agda-2.1.2...
dist/build/Syntax/Parser/Parser.hs:29:0:
error: ../../undefined.h: No such file or directory
Original issue reported on code.google.com by [email protected] on 29 Dec 2007 at 4:31
It should be possible to detect termination when an argument is smaller
than a dotted pattern. For instance, the following code should terminate:
module Test where
data Nat : Set where
zero : Nat
suc : Nat → Nat
data Bool : Set where
true : Bool
false : Bool
_&&_ : Bool → Bool → Bool
true && b = b
false && b = false
data Ty : {_ : Nat} → Set where
Base : forall {n} → Ty {suc n}
Arr : forall {n} → Ty {n} → Ty {n} → Ty {suc n}
subty : forall {n} → Ty {n} → Ty {n} → Bool
subty Base Base = true
subty (Arr σ τ) (Arr σ’ τ’) = subty σ’ σ && subty τ τ’
subty _ _ = false
Currently the termination checker cannot see that in both the two recursive
calls of subty the first (hidden) argument is strictly smaller than on the LHS.
Andreas: Discussed that with Ulf. The internal syntax erases the dotted
patterns constructed during pattern checking. This is an optimization for
speeding up execution, but the “logical” reading (fully reconstruced form)
of the second clause is
subty {suc n} (Arr {n} σ τ) (Arr {n} σ’ τ’) = subty {n} σ’ σ && subty {n} τ τ’
To keep internally a fully reconstructed form is probably not only useful
for the termination checker but also for other static analyses.
To print back the fully reconstructed form, as for instance Twelf does, is
also a good feedback to the user: He sees how the system “understood” his
input, and he can check that it understood it correctly. See <a
href=http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.PrintReconstr
uctedTerms>Main.PrintReconstructedTerms
</a> feature request.
Original issue reported on code.google.com by [email protected] on 24 Oct 2007 at 10:40
The command-line interactive interface (agda -I) does not give a
warning when the following module is loaded, even though there is an
unsolved meta-variable.
module Bug where
a : Set
a = _
Original issue reported on code.google.com by nils.anders.danielsson on 25 Feb 2008 at 7:00
Examples:
- Literate mode
- ? + ?
- {- -- -}
Original issue reported on code.google.com by [email protected] on 24 Oct 2007 at 11:02
At the moment termination checking can be disabled for a particular file
using the OPTIONS pragma. It would be nice if you could do this on the
declaration level. Something like
{-# NO_TERMINATION_CHECK #-}
mutual
...
The pragma would disable termination checking for the following mutual block.
Original issue reported on code.google.com by [email protected] on 24 Oct 2007 at 4:54
The last definition in this file (composition of natural transformations)
causes command line agda to
stack overflow
Original issue reported on code.google.com by [email protected] on 29 Nov 2007 at 10:42
Attachments:
f : Nat -> Nat -> Nat
f (suc n) m with y
where
y = n + m
f (suc n) m | x = {!y !}
where
z = n
Issues
* y is in scope in the second clause
* the type depends on whether or not the second where is present
- if present: Nat
- otherwise: (n m : Nat) -> Nat
Original issue reported on code.google.com by [email protected] on 25 Oct 2007 at 9:58
What the summary says.
Original issue reported on code.google.com by [email protected] on 24 Oct 2007 at 11:00
1) Load the following program using the GUI:
{-# OPTIONS --dont-termination-check #-}
module Bug where
bot : Set
bot = bot
2) Remove the pragma and reload. The nonterminating function bot is not
highlighted.
Original issue reported on code.google.com by nils.anders.danielsson on 8 Nov 2007 at 8:15
The name x is exported twice from Bug, making it impossible to use.
Agda should issue an error here.
module Bug where
module A where
postulate x : Set
module B where
postulate x : Set
open A public
open B public
Original issue reported on code.google.com by nils.anders.danielsson on 7 Dec 2007 at 3:47
On line 37 p should be of type False, but Agda cannot see it
I even changed the def. of <N to make this more explicit but it didn't make
a difference
If I write acc-zero _ () instead I get
.x <N zero should be empty, but it isn't (as far as I can see)
but I do not understand why it cannot is it
Original issue reported on code.google.com by [email protected] on 26 Nov 2007 at 3:39
Attachments:
module Bug where
module Dummy {A : Set1} where
postulate D : Set
-- This works:
T : Set
T = Dummy.D {Set}
-- This doesn't:
-- T' : Set
-- T' = Dummy.D {A = Set}
Original issue reported on code.google.com by nils.anders.danielsson on 10 Mar 2008 at 4:33
The current rule for checking interaction metas against implicit function
spaces is
x : A |- newHole (a : B)
----------------------------------
? : {x : A} -> B --> \{x} -> a
It would make sense to change this so that it doesn't insert the implicit
lambda.
Original issue reported on code.google.com by [email protected] on 19 Nov 2007 at 11:40
Truncate a valid interface file to just the first eight bytes, and make
Agda try to read this file. You will get the following error:
agda: user error (Codec.Compression.Zlib: premature end of compressed stream)
This can most likely be fixed by forcing the entire interface in
Interaction.Imports.readInterface.
Truncated interface files occur in practice, since Agda sometimes runs out
of stack space when trying to write an interface file. (This might also be
a bug.)
Original issue reported on code.google.com by nils.anders.danielsson on 12 Nov 2007 at 8:51
I tried to define thinning for a fragment of a typed syntax for dependent types:
In the attached fil the penultimate line doesn't type check because (at least)
agda is not
computing the line "nil' = nil" (this line is necessary to get around
constructors of data types not
being in scope of the types of mutually defined functions.
If you insert text after the comment on the penultimate line into the goal on
the same line it and
do "C-u C-c C-d" then the expression "thin⁺ nil' σ ρ" has type "Ty (insert
nil' σ)". "nil'" should
compute to "nil" and "insert nil σ" should then compute to "Γ < σ" and it
should then have the
right type.
At least I think it should!
Original issue reported on code.google.com by [email protected] on 11 Jan 2008 at 2:59
Attachments:
The following little file type checks:
data Ty : Set where
ι : Ty
_→_ : Ty -> Ty -> Ty
data Con : Set where
ε : Con
_<_ : Con -> Ty -> Con
data Var : Con -> Ty -> Set where
vZ : forall {Γ σ} -> Var (Γ < σ) σ
vS : forall {Γ σ}{τ : Ty} -> Var Γ σ -> Var (Γ < τ) σ
stren : forall {Γ σ} -> Var Γ σ -> Con
stren (vZ {Γ}) = Γ
stren (vS {τ = τ} v) = stren v < τ
_/_ : forall Γ {σ} -> Var Γ σ -> Con
Γ / v = stren v
thin : forall {Γ σ τ}(v : Var Γ σ) -> Var (Γ / v) τ -> Var Γ τ
thin vZ v' = vS v'
thin (vS v) vZ = vZ
thin (vS v) (vS v') = vS (thin v v')However if I make stren a local function:
_/_ : forall Γ {σ} -> Var Γ σ -> Con
Γ / v = stren v where
stren : forall {Γ σ} -> Var Γ σ -> Con
stren (vZ {Γ}) = Γ
stren (vS {τ = τ} v) = stren v < τThen the definition of thin doesn't type check anymore highlighting the v' on the right hand side of the last line:
(.Γ < .τ) != .Γ of type Con
when checking that the expression v' has type
Var (.Γ / v) (_79 v v')
Also if I change thin to:
thin vZ v' = vS v'
thin (vS v) v' = ? and examine the context of the produced goal the type of v' looks a bit weird:
v' : Var (.Bug._.stren (.Γ < .τ) (vS v) (vS v)) .τ
``
making stren global again yields:
v' : Var (stren (vS v)) .τ
``
The function stren is rather pointless... but that's beside the point :)
Original issue reported on code.google.com by [email protected] on 9 Jan 2008 at 5:44
module Bug where
module A (x : Set) where
postulate
a : Set
record B (x : Set) : Set where
open A x
field
f : a
Error message:
Bug.agda:10,9-10
Set -> Set != _6 of type Set1
when checking that the expression a has type _6
Original issue reported on code.google.com by nils.anders.danielsson on 7 Dec 2007 at 12:59
Pattern matching against natural number literals doesn't work properly. For
instance:
f : Nat -> Nat
f 0 = zero
f (suc n) = n
Here, f (suc n) for neutral n will not reduce.
Original issue reported on code.google.com by [email protected] on 22 Nov 2007 at 3:04
I define the record
record DLO : Set1 where
I : Set
_<_ : I -> I -> Bool
irreflL : (a : I) -> F(a < a)
transL : {a b c : I} -> T(a < b) -> T(b < c) -> T(a < c)
linear : {a b c : I}-> F(a < b) -> F(b < c) -> F(a < c)
I want now to construct an elem of this record
record{ I = True;
_<_ = \(a b : True) -> false;
irreflL = ?;
transL = ?;
linear = ?
}
Bug 1) If I have "?;" then emacs agda will go well but will not put the ?
in a green box
Bug 2) If I want to refine any of the last 2 ? with "\{a b c} p q -> ?"
agda will do refine as "(\{a b c} p q -> ?) ?"
Seems that if I only want to refine with "\p q -> ?" it works OK
Original issue reported on code.google.com by [email protected] on 16 Nov 2007 at 1:36
module Bug where
infix 4 _≡_
data _≡_ {a : Set} (x : a) : a -> Set where
≡-refl : x ≡ x
postulate
≡-subst : {a : Set} -> (P : a -> Set)
-> forall {x y} -> x ≡ y -> P x -> P y
Kind : Set
simple : Kind
Ty : Kind -> Set
⊢_ : forall {k} -> Ty k -> Set
⌜_⌝⋆ : Ty simple -> Ty simple
lemma : forall τ -> τ ≡ ⌜ τ ⌝⋆
module SubstDef (• : forall {k} -> Ty k -> Set) where
postulate SubstKit : Set
module Subst {• : forall {k} -> Ty k -> Set}
(kit : SubstDef.SubstKit •) where
infixl 48 _/⊢
postulate
_/⊢ : forall {τ : Ty simple} -> ⊢ τ -> ⊢ τ
postulate
varKit : SubstDef.SubstKit ⊢_
open module VarSubst = Subst varKit
data ⊢↦_ : forall {k} -> Ty k -> Set where
foo : (τ : Ty simple) -> ⊢ τ -> ⊢↦ τ
postulate
↦_ : forall {τ : Ty simple} -> ⊢ τ -> ⊢↦ τ
⌜_⌝↦ : forall {τ} -> ⊢↦ τ -> ⊢↦ ⌜ τ ⌝⋆
⌜ foo τ e ⌝↦ = ↦ ≡-subst ⊢_ (lemma τ) e
_/⊢↦ : forall {k} {τ : Ty k} -> ⊢↦ τ -> ⊢↦ τ
(foo τ e) /⊢↦ = foo τ (e /⊢)
⌜/⊢↦⌝-lemma : forall {σ : Ty simple} (e : ⊢↦ σ)
-> (⌜ e ⌝↦ /⊢↦) ≡ (⌜ e /⊢↦ ⌝↦)
⌜/⊢↦⌝-lemma (foo τ e) = helper τ e ⌜ τ ⌝⋆ (lemma τ)
where
helper
: forall (τ : Ty simple) (e : ⊢_ {simple} τ) (σ : Ty simple)
-> (eq : τ ≡ σ)
-> _≡_ {⊢↦_ {simple} σ}
(_/⊢↦ {simple} {σ}
(↦_ {σ} (≡-subst {Ty simple} (⊢_ {simple}) {τ} {σ}
eq e)))
(↦_ {σ} (≡-subst {Ty simple} (⊢_ {simple}) {τ} {σ}
eq (Subst._/⊢ {\{k} x -> ⊢_ {k} x}
varKit {τ} e)))
helper τ e ._ ≡-refl = rhs
where postulate rhs : _
⌜/⊢↦⌝-lemma (foo τ e) with ⌜ τ ⌝⋆ | lemma τ
... | ._ | ≡-refl = rhs
where postulate rhs : _
-- The generation of a local with function fails here. The function
-- generated is almost identical to the function "helper" above, with
-- the exception that the eta-expanded version of ⊢_ towards the end
-- has become {\k x -> ⊢_ {k} x} instead of {\{k} x -> ⊢_ {k} x}.
Original issue reported on code.google.com by nils.anders.danielsson on 19 Oct 2007 at 3:18
The module Bug for some reason yields the following error message:
Bug.agda:17,7–10
No binding for builtin thing ZERO, use {-# BUILTIN ZERO name #-} to
bind it to ‘name’
when checking that the expression bar has type 0 ≡ 0
If a BUILTIN ZERO pragma is added (see Bug2), then Agda panics:
Bug2.agda:25,7–10
Panic: Pattern match failure in do expression at
src/full/TypeChecking/Conversion.hs:119:6–29
when checking that the expression bar has type 0 ≡ 0
The modules are defined as follows:
module Bug where
postulate
ℤ : Set
Float : Set
_≡_ : ℤ → ℤ → Set
{-# BUILTIN INTEGER ℤ #-}
{-# BUILTIN FLOAT Float #-}
primitive primRound : Float → ℤ
ℤ−0 : ℤ
ℤ−0 = primRound 0.0
foo : ℤ−0 ≡ ℤ−0
foo = bar
where postulate bar : ℤ−0 ≡ ℤ−0
module Bug2 where
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}
postulate
ℤ : Set
Float : Set
_≡_ : ℤ → ℤ → Set
{-# BUILTIN INTEGER ℤ #-}
{-# BUILTIN FLOAT Float #-}
primitive primRound : Float → ℤ
ℤ−0 : ℤ
ℤ−0 = primRound 0.0
foo : ℤ−0 ≡ ℤ−0
foo = bar
where postulate bar : ℤ−0 ≡ ℤ−0
Original issue reported on code.google.com by [email protected] on 24 Oct 2007 at 10:46
-- Contrived example:
module Panic where
data [_] (a : Set) : Set where
[] : [ a ]
_∷_ : a -> [ a ] -> [ a ]
data Ty : Set where
id : Ty
_→_ : Ty -> Ty -> Ty
fun : [ Ty ] -> Ty -> Ty
fun [] τ = τ
fun (σ ∷ σs) τ = σ → fun σs τ
data T : Ty -> Set where
c₁ : forall ts -> T (fun ts id)
c₂ : T (id → id)
foo : forall ts {a} -> T (fun ts a) -> _
foo (._ ∷ []) c₂ = ?
-- Error message:
-- Panic.agda:20,1-21
-- Panic: failed to split: CantSplit Panic.c₁
-- when checking the definition of foo
-- The error message should be improved.
Original issue reported on code.google.com by nils.anders.danielsson on 10 Mar 2008 at 4:37
No error message is issued, even though _+_ is not declared in the
record:
module Bug where
record R : Set where
infixl 6 _+_
Original issue reported on code.google.com by nils.anders.danielsson on 7 Dec 2007 at 1:37
{-# OPTIONS --dont-termination-check #-}
module Foo where
f : Set
f = ?
Loading this file with C-x-l doesn't turn the question mark into a nice green
shed. It just stays
as a question mark. Removing the pragma and reloading causes the shed to appear.
module Foo where
f : Set
f = { }0
I wonder if this is related to Defect 20...
James
Original issue reported on code.google.com by [email protected] on 21 Nov 2007 at 4:58
This slightly longer file than the one in issue 29 upsets the emacs mode.
Trying to load it gives the
error "end of file during parsing" which appears in the minibuffer at the
bottom. Specifically it is
the contents of the id field in the last definition of AlgCal that triggers the
problem.
Original issue reported on code.google.com by [email protected] on 2 Dec 2007 at 5:41
Attachments:
Running
Agda2/examples/AIM6/RegExp/talk> agda -v9 SimpleMatcher.agda
agda: unbound variable
The bug must be in TypeChecking/Conversion.hs
Original issue reported on code.google.com by [email protected] on 24 Oct 2007 at 10:52
module Bug where
record M : Set1 where
field
f : Set
module MOps (m : M) where
open M m public
postulate m : M
-- This works:
-- private
-- module MO = MOps m
-- open MO hiding (f)
-- open MO public using (f)
-- This works:
-- open MOps m using (f)
-- open MOps m hiding (f)
-- This doesn't:
open MOps m hiding (f)
open MOps m using (f)
postulate foo : f -> Set
--------------------
Error message:
Ambiguous name f. It could refer to any one of
.Bug._._.f bound at /home/nad/work/lib/Bug.agda:5,5-6
_._.f bound at /home/nad/work/lib/Bug.agda:5,5-6
when scope checking f
Original issue reported on code.google.com by nils.anders.danielsson on 30 Nov 2007 at 10:40
What steps will reproduce the problem?
1. Define this module:
module bug where
A : Set
A = A -- non-terminating definition should give an error, not a loop
q : A
q = ? -- including this definition makes agda loop
2. run agda bug.agda
What is the expected output? What do you see instead?
An error like "bug.A does NOT pass the termination check".
Instead, agda loops.
What version of the product are you using? On what operating system?
Agda 2 version 2.1.3
compiled from darcs repo 071212 or so.
Please provide any additional information below.
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.
/Patrik
Original issue reported on code.google.com by [email protected] on 17 Dec 2007 at 9:48
record X : Set1 where
field Y : Set
src/full/Interaction/Highlighting/Generate.hs:195: the impossible
happened
Original issue reported on code.google.com by [email protected] on 29 Nov 2007 at 10:39
The following program type checks, both in batch and in interactive mode:
module Bug where
abstract
T : Set -> Set
T a = a
data Foo (a : Set) : Set where
foo : T (Foo a) -> Foo aOriginal issue reported on code.google.com by nils.anders.danielsson on 19 Oct 2007 at 6:38
The names mentioned in fixity declarations are not checked to exist. For
instance:
module Bug where
infixl 40 _foo_
Original issue reported on code.google.com by [email protected] on 18 Oct 2007 at 2:35
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
Django
The Web framework for perfectionists with deadlines.
Laravel
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft
Open source projects and samples from Microsoft.
Google
Google ❤️ Open Source for everyone.
Alibaba
Alibaba Open Source for everyone
D3
Data-Driven Documents codes.
Tencent
China tencent open source team.