Setup:
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat
module M (X : Set) where
record Foo : Set where
no-eta-equality
constructor inc
field foo1 foo2 : X
{-# INLINE Foo.constructor #-}
open Foo
to : X → X → Foo
{-# INLINE to #-}
to a b = record { foo1 = a ; foo2 = b }
module N (X : Set) where
open M X public
open N Nat
Punchline:
x : M.Foo Nat x = M.to Nat 1 2 -- fails: -- _ : x ≡ M.inc 1 2 -- _ = refl y : N.Foo Nat y = N.to Nat 1 2 -- fails: -- _ : y ≡ M.inc 1 2 -- _ = refl z : Foo z = to 1 2 -- works?! _ : z ≡ inc 1 2 _ = refl
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4