[Agda] uniform normalization

[Ulf Norell]

The improved reflection, which you can read about here:

http://agda.readthedocs.org/en/latest/language/reflection.html

/ Ulf

On Mon, Apr 11, 2016 at 10:08 PM, Bradley Hardy <bch29 at cam.ac.uk> wrote:

> By the new tactic language, do you mean the improved reflection
> capabilities in 2.5, or has something more Coq-like recently been
> implemented?
>
>
> > On 11 Apr 2016, at 20:14, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> >
> > Since (f n) does not reduce to 0 (both equations are more specific), you
> have to split on n.
> >
> > You could implement a tactic using Agda's new tactic language that does
> such routine jobs for you.
> >
> > On 11.04.2016 18:28, Sergei Meshveliani wrote:
> >> Hello, All.
> >>
> >> I have the following question.
> >> The program
> >>
> >> -------------------------------------------------
> >> open import Relation.Binary.PropositionalEquality
> >> open import Data.Nat
> >>
> >> f : ℕ → ℕ
> >> f 0       = 0
> >> f (suc _) = 0
> >>
> >> theorem :  ∀ n → f n ≡ 0
> >> theorem _ =  refl
> >> --------------------------------------------------
> >>
> >> is not type-checked, because Agda expects the two proofs to be given.
> >> One for the case 0, another for the case (suc _).
> >> Both proofs can be set `refl', that is -- by normalization.
> >>
> >> Could the type checker check the proof by a single `refl', by
> >> normalizing each branch?
> >> (this will simplify many proofs).
> >>
> >> Thanks,
> >>
> >> ------
> >> Sergei
> >>
> >> _______________________________________________
> >> Agda mailing list
> >> Agda at lists.chalmers.se
> >> https://lists.chalmers.se/mailman/listinfo/agda
> >>
> >
> >
> > --
> > Andreas Abel  <><      Du bist der geliebte Mensch.
> >
> > Department of Computer Science and Engineering
> > Chalmers and Gothenburg University, Sweden
> >
> > andreas.abel at gu.se
> > http://www2.tcs.ifi.lmu.de/~abel/
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160411/f9dedcf5/attachment.html