Agda-2.2.10: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.Auto.CaseSplit
Documentation
data
HI
a
Source
Constructors
HI
FMode
a
type
CSPat
o =
HI
(
CSPatI
o)
Source
type
CSCtx
o = [
HI
(
MId
,
MExp
o)]
Source
data
CSPatI
o
Source
Constructors
CSPatConApp
(
ConstRef
o) [
CSPat
o]
CSPatVar
Nat
CSPatExp
(
MExp
o)
CSWith
(
MExp
o)
CSAbsurd
CSOmittedArg
type
Sol
o = [(
CSCtx
o, [
CSPat
o],
Maybe
(
MExp
o))]
Source
caseSplitSearch
::
forall
o.
IORef
Int
->
Int
-> [
ConstRef
o] ->
Maybe
(
EqReasoningConsts
o) ->
Int
->
Int
->
ConstRef
o ->
CSCtx
o ->
MExp
o -> [
CSPat
o] ->
IO
[
Sol
o]
Source
caseSplitSearch'
::
forall
o. (
Int
->
CSCtx
o ->
MExp
o -> ([
Nat
],
Nat
, [
Nat
]) ->
IO
(
Maybe
(
MExp
o))) ->
Int
->
Int
->
ConstRef
o ->
CSCtx
o ->
MExp
o -> [
CSPat
o] ->
IO
[
Sol
o]
Source
infertypevar
::
CSCtx
o ->
Nat
->
MExp
o
Source
replace
::
Nat
->
Nat
->
MExp
o ->
MExp
o ->
MExp
o
Source
betareduce
::
MExp
o ->
MArgList
o ->
MExp
o
Source
eqelr
::
Elr
o ->
Elr
o ->
Bool
Source
replacep
::
Nat
->
Nat
->
CSPatI
o ->
MExp
o ->
CSPat
o ->
CSPat
o
Source
rm
::
MM
a b -> a
Source
mm
:: a ->
MM
a b
Source
unifyexp
::
MExp
o ->
MExp
o ->
Maybe
[(
Nat
,
MExp
o)]
Source
lift
::
Nat
->
MExp
o ->
MExp
o
Source
removevar
::
CSCtx
o ->
MExp
o -> [
CSPat
o] -> [(
Nat
,
MExp
o)] -> (
CSCtx
o,
MExp
o, [
CSPat
o])
Source
notequal
::
Nat
->
Nat
->
MExp
o ->
MExp
o ->
IO
Bool
Source
findperm
:: [
MExp
o] ->
Maybe
[
Nat
]
Source
freevars
::
MExp
o -> [
Nat
]
Source
applyperm
:: [
Nat
] ->
CSCtx
o ->
MExp
o -> [
CSPat
o] -> (
CSCtx
o,
MExp
o, [
CSPat
o])
Source
rename
:: (
Nat
->
Nat
) ->
MExp
o ->
MExp
o
Source
renamep
:: (
Nat
->
Nat
) ->
CSPat
o ->
CSPat
o
Source
seqctx
::
CSCtx
o ->
CSCtx
o
Source
depthofvar
::
Nat
-> [
CSPat
o] ->
Nat
Source
localTerminationEnv
:: [
CSPat
o] -> ([
Nat
],
Nat
, [
Nat
])
Source
localTerminationSidecond
:: ([
Nat
],
Nat
, [
Nat
]) ->
ConstRef
o ->
MExp
o ->
EE
(
MyPB
o)
Source
getblks
::
MExp
o ->
IO
[
Nat
]
Source
Produced by
Haddock
version 2.6.1