Assignees
Description{-# OPTIONS --rewriting --confluence-check #-}
module Test45 where
open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
{-# BUILTIN REWRITE _≡_ #-}
p : true ≡ false
q : true ≡ false
p = q
{-# REWRITE p #-}
q = refl
HarrisonGrodin, jespercockx, mietek, NathanielB123 and Jesin
Metadata Metadata Development No branches or pull requests Issue actionsYou can’t perform that action at this time.
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