I'm trying to rewrite by a constructor which seems to hit an __IMPOSSIBLE__. Using Agda version 2.7.0.
{-# OPTIONS --rewriting #-}
data One : Set where
⊤ : One
data P : One → One → Set where
m : P ⊤ ⊤
{-# BUILTIN REWRITE P #-}
p = m
{-# REWRITE p #-} -- this is ok
--{-# REWRITE m #-} -- this is not ok
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