[Agda] Inspect.

[Andreas Abel]

Frankly, I do not know.  We could replace the current definition by your 
simplification, provided that both work equally well wrt. unification. 
Did you do the experiments?

Cheers,
Andreas

On 27.12.2014 17:52, flicky frans wrote:
> Hello. I am probably missing something obvious, but why `inspect' is
> not defined like this?
>
> record Reveal_·_is_ {α β} {A : Set α} {B : A -> Set β}
>    (f : (x : A) -> B x) (x : A) (y : B x) : Set (α ⊔ β) where
>      constructor [_]
>      field eq : f x ≡ y
>
> inspect : ∀ {α β} {A : Set α} {B : A -> Set β}
>          -> (f : (x : A) -> B x) -> (x : A) -> Reveal f · x is f x
> inspect f x = [ refl ]
>
> This looks simpler and still allows you to pattern-match on (f x) and
> to remember, that (f x ≡ y).
> _______________________________________________
> 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/