Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/induction-ex.agda @ 405:af8f630b7e60

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 18:02:04 +0900
parents cd73fe566291
children
comparison
equal deleted inserted replaced
404:dfaf230f7b9a 405:af8f630b7e60
1 {-# OPTIONS --guardedness --sized-types #-} 1 {-# OPTIONS --cubical-compatible --guardedness --sized-types #-}
2
2 module induction-ex where 3 module induction-ex where
3 4
4 open import Relation.Binary.PropositionalEquality 5 open import Relation.Binary.PropositionalEquality
5 open import Size 6 open import Size
6 open import Data.Bool 7 open import Data.Bool