ulfnorell / agda-test Goto Github PK
View Code? Open in Web Editor NEWAgda test
Agda test
From [email protected] on November 04, 2007 20:44:18
For example
postulate test :
Set
generates a parse error
Original issue: http://code.google.com/p/agda/issues/detail?id=18
From [email protected] on November 29, 2007 23:51:40
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 f
I think that the original p should get replaced by _ in the helper function if its name has been
captured.
Original issue: http://code.google.com/p/agda/issues/detail?id=30
From nils.anders.danielsson on March 10, 2008 17:37:00
-- 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: http://code.google.com/p/agda/issues/detail?id=50
From nils.anders.danielsson on March 10, 2008 17:33:55
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: http://code.google.com/p/agda/issues/detail?id=49
From nils.anders.danielsson on December 07, 2007 14:37:36
No error message is issued, even though + is not declared in the
record:
module Bug where
record R : Set where
infixl 6 +
Original issue: http://code.google.com/p/agda/issues/detail?id=35
From [email protected] on October 24, 2007 12:52:44
Running
Agda2/examples/AIM6/RegExp/talk> agda -v9 SimpleMatcher.agda
agda: unbound variable
The bug must be in TypeChecking/Conversion.hs
Original issue: http://code.google.com/p/agda/issues/detail?id=12
From [email protected] on November 26, 2007 16:39:31
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
Attachment: test.agda
Original issue: http://code.google.com/p/agda/issues/detail?id=27
From [email protected] on October 24, 2007 12:34:58
What the summary says.
Original issue: http://code.google.com/p/agda/issues/detail?id=6
From [email protected] on January 09, 2008 18:44:06
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: http://code.google.com/p/agda/issues/detail?id=44
From [email protected] on December 02, 2007 18:41:08
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.
Attachment: CategoriesandMonads.agda
Original issue: http://code.google.com/p/agda/issues/detail?id=32
From [email protected] on November 29, 2007 23:39:40
record X : Set1 where
field Y : Set
src/full/Interaction/Highlighting/Generate.hs:195: the impossible
happened
Original issue: http://code.google.com/p/agda/issues/detail?id=28
From [email protected] on October 24, 2007 12:50:19
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
Attachment: Bug.agda
Original issue: http://code.google.com/p/agda/issues/detail?id=11
From [email protected] on November 29, 2007 23:42:35
The last definition in this file (composition of natural transformations) causes command line agda to
stack overflow
Attachment: Categories.agda
Original issue: http://code.google.com/p/agda/issues/detail?id=29
From [email protected] on October 24, 2007 12:46:38
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: http://code.google.com/p/agda/issues/detail?id=10
From [email protected] on October 24, 2007 12:37:07
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: http://code.google.com/p/agda/issues/detail?id=7
From [email protected] on October 24, 2007 13:00:34
What the summary says.
Original issue: http://code.google.com/p/agda/issues/detail?id=14
From [email protected] on January 26, 2008 02:18:32
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: http://code.google.com/p/agda/issues/detail?id=46
From [email protected] on October 24, 2007 12:54:44
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: http://code.google.com/p/agda/issues/detail?id=13
From [email protected] on November 22, 2007 16:04:23
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: http://code.google.com/p/agda/issues/detail?id=26
From [email protected] on January 27, 2008 17:34:07
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: http://code.google.com/p/agda/issues/detail?id=47
From nils.anders.danielsson on February 25, 2008 20:00:57
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: http://code.google.com/p/agda/issues/detail?id=48
From [email protected] on December 29, 2007 17:31:01
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: http://code.google.com/p/agda/issues/detail?id=43
From [email protected] on November 19, 2007 12:40:35
The current rule for checking interaction metas against implicit function
spaces is
? : {x : A} -> B --> {x} -> a
It would make sense to change this so that it doesn't insert the implicit
lambda.
Original issue: http://code.google.com/p/agda/issues/detail?id=24
From nils.anders.danielsson on December 11, 2007 01:24:53
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: http://code.google.com/p/agda/issues/detail?id=37
From nils.anders.danielsson on October 19, 2007 17:10:51
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: http://code.google.com/p/agda/issues/detail?id=2
From [email protected] on October 18, 2007 16:35:18
The names mentioned in fixity declarations are not checked to exist. For
instance:
module Bug where
infixl 40 foo
Original issue: http://code.google.com/p/agda/issues/detail?id=1
From [email protected] on January 11, 2008 15:59:15
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!
Attachment: DependentThinning.agda
Original issue: http://code.google.com/p/agda/issues/detail?id=45
From [email protected] on October 25, 2007 11:58:28
f : Nat -> Nat -> Nat
f (suc n) m with y
where
y = n + m
f (suc n) m | x = {!y !}
where
z = n
Issues
Original issue: http://code.google.com/p/agda/issues/detail?id=17
From [email protected] on October 24, 2007 12:44:47
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: http://code.google.com/p/agda/issues/detail?id=9
From nils.anders.danielsson on November 08, 2007 21:15:26
{-# OPTIONS --dont-termination-check #-}
module Bug where
bot : Set
bot = bot
Original issue: http://code.google.com/p/agda/issues/detail?id=20
From [email protected] on November 16, 2007 14:36:08
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: http://code.google.com/p/agda/issues/detail?id=22
From nils.anders.danielsson on November 12, 2007 21:51:04
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: http://code.google.com/p/agda/issues/detail?id=21
From nils.anders.danielsson on December 07, 2007 13:59:38
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: http://code.google.com/p/agda/issues/detail?id=34
From [email protected] on October 24, 2007 13:02:36
Examples:
Original issue: http://code.google.com/p/agda/issues/detail?id=15
From [email protected] on December 17, 2007 10:48:29
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
/Patrik
Original issue: http://code.google.com/p/agda/issues/detail?id=42
From nils.anders.danielsson on December 11, 2007 17:02:10
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: http://code.google.com/p/agda/issues/detail?id=39
From nils.anders.danielsson on October 19, 2007 20:38:31
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 a
Original issue: http://code.google.com/p/agda/issues/detail?id=4
From [email protected] on November 06, 2007 14:34:50
*** 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: http://code.google.com/p/agda/issues/detail?id=19
From [email protected] on November 21, 2007 17:58:28
{-# 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: http://code.google.com/p/agda/issues/detail?id=25
From [email protected] on November 17, 2007 14:56:01
The literate agda files yield a lexical error (after to compile with ghc 6.8.1)
Version: Darcs repository on 20071117
Original issue: http://code.google.com/p/agda/issues/detail?id=23
From nils.anders.danielsson on December 11, 2007 20:38:29
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: http://code.google.com/p/agda/issues/detail?id=41
From nils.anders.danielsson on December 11, 2007 15:38:22
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: http://code.google.com/p/agda/issues/detail?id=38
From [email protected] on October 24, 2007 12:40:20
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.PrintReconstructedTerms>Main.PrintReconstructedTerms feature request.
Original issue: http://code.google.com/p/agda/issues/detail?id=8
From [email protected] on October 24, 2007 18:54:11
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: http://code.google.com/p/agda/issues/detail?id=16
From nils.anders.danielsson on December 11, 2007 20:19:30
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: http://code.google.com/p/agda/issues/detail?id=40
From nils.anders.danielsson on December 07, 2007 16:47:30
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: http://code.google.com/p/agda/issues/detail?id=36
From [email protected] on December 04, 2007 14:56:54
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: http://code.google.com/p/agda/issues/detail?id=33
From [email protected] on October 24, 2007 12:32:42
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: http://code.google.com/p/agda/issues/detail?id=5
From nils.anders.danielsson on October 19, 2007 17:18:08
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: http://code.google.com/p/agda/issues/detail?id=3
From nils.anders.danielsson on November 30, 2007 11:40:36
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: http://code.google.com/p/agda/issues/detail?id=31
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 is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
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.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.