open import Data.Nat
open import Data.Empty
hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
open import Data.Nat | |
open import Data.Empty | |
hiding (⊥-elim) | |
open import Relation.Nullary | |
open import Relation.Binary.PropositionalEquality | |
hiding ([_]) | |
infix 3 _⊢_ _=β_ | |
infixr 7 _→̇_ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE FlexibleContexts, FlexibleInstances #-} | |
{-# LANGUAGE TypeInType , ScopedTypeVariables , TypeFamilies, TypeOperators #-} | |
{-# LANGUAGE GADTs, StandaloneDeriving #-} | |
{-# LANGUAGE Safe #-} | |
module Unification where | |
import Data.Kind | |
import Prelude hiding ((++)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE FlexibleContexts, BangPatterns #-} | |
import Data.IntMap.Strict | |
import Data.Maybe | |
import Data.Function | |
import Control.Monad.Identity | |
import Control.Monad.State.Lazy hiding (fix) | |
import Prelude hiding (lookup) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{- Coquand, T., & Dybjer, P. (1997). Intuitionistic model constructions and normalization proofs. | |
Mathematical Structures in Computer Science, 7(1). https://doi.org/10.1017/S0960129596002150 -} | |
open import Data.Empty using (⊥) | |
open import Data.Unit using (⊤; tt) | |
open import Data.Nat using (ℕ; zero; suc) | |
open import Data.Product using (_×_; _,_; Σ; proj₁; proj₂; ∃-syntax) | |
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong) | |
infix 3 _-→_ _-↛_ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE ViewPatterns #-} | |
{-# LANGUAGE PatternSynonyms #-} | |
import Data.Vector as V | |
pattern Empty :: Vector a | |
pattern Empty <- (V.null -> True) where Empty = V.empty | |
uncons :: Vector a -> Maybe (a, Vector a) | |
uncons Empty = Nothing |
Evil mode overwrites the mouse-2 event which is used by Agda to go to the definition of clicked identifier.
To restore the desired behavioru, just add the following line after enabling Evil (require 'evil)
(define-key evil-normal-state-map [mouse-2] 'agda2-goto-definition-mouse)
OlderNewer